image for world intro

pull/251/merge
Jon Eugster 9 months ago
parent 02d0d57453
commit 096bd55f9b

@ -101,7 +101,7 @@ function Game() {
{<>
<ChatPanel visible={worldId ? (levelId == 0 && page == 1) :(page == 0)} />
{ worldId ?
(levelId > 0 && <LevelWrapper visible={page == 1} />) :
<LevelWrapper visible={page == 1} /> :
<WorldTreePanel visible={page == 1} />
}
<InventoryPanel visible={page == 2} />
@ -113,7 +113,7 @@ function Game() {
<ChatPanel />
<div className="column">
{/* Note: apparently without this `div` the split panel bugs out. */}
{worldId ? (levelId > 0 && <LevelWrapper />) : <WorldTreePanel /> }
{worldId ? <LevelWrapper /> : <WorldTreePanel /> }
</div>
<InventoryPanel />
</Split>

@ -34,7 +34,6 @@ import { ChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
ProofContext, PageContext } from './infoview/context'
import { DualEditor, ExerciseStatement } from './infoview/main'
import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api'
import { DeletedHints, Hints, MoreHelpButton } from './hints'
import path from 'path';
import '@fontsource/roboto/300.css'

Loading…
Cancel
Save