cleanup; including cleaning up chat

client/src/app.tsx

@@ -1,6 +1,6 @@
 import * as React from 'react';
 import { Outlet, useParams, useSearchParams } from "react-router-dom";
-import { useEffect, useState } from 'react';
+import { Suspense, useEffect, useState } from 'react';
 
 import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
@@ -13,7 +13,7 @@ import { PageContext, PreferencesContext} from './components/infoview/context';
 import UsePreferences from "./state/hooks/use_preferences"
 import { Navigation } from './components/navigation';
 import { useSelector } from 'react-redux';
-import { changeTypewriterMode, selectOpenedIntro, selectTypewriterMode } from './state/progress';
+import { changeTypewriterMode, selectReadIntro, selectTypewriterMode } from './state/progress';
 import { useAppDispatch } from './hooks';
 import { Popup, PopupContext } from './components/popup/popup';
 import { useGetGameInfoQuery } from './state/api';
@@ -45,7 +45,7 @@ function App() {
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const [searchParams, setSearchParams] = useSearchParams()
 
-  const openedIntro = useSelector(selectOpenedIntro(gameId))
+  const readIntro = useSelector(selectReadIntro(gameId, worldId))
 
   // mobile only: game intro should only be shown once and skipped afterwards
   useEffect(() => {
@@ -53,14 +53,14 @@ function App() {
       console.log('setting page to 1')
       setPage(1)
     } else {
-      if (openedIntro && page == 0) {
+      if (readIntro && page == 0) {
         console.log('setting page to 1')
         setPage(1)
       } else {
         // setPage(0)
       }
     }
-  }, [openedIntro, worldId, levelId])
+  }, [worldId, levelId])
 
   // option to pass language as `?lang=de` in the URL
   useEffect(() => {

client/src/components/chat.tsx

@@ -1,15 +1,19 @@
 import * as React from 'react'
-import { PageContext, PreferencesContext } from './infoview/context'
+import { ChatContext, PageContext, PreferencesContext, ProofContext } from './infoview/context'
 import { GameIdContext } from '../app'
 import { useTranslation } from 'react-i18next'
-import { useAppDispatch } from '../hooks'
-import { Hint } from './hints'
+import { useAppDispatch, useAppSelector } from '../hooks'
 import { Button } from './button'
-import { changedOpenedIntro } from '../state/progress'
+import { changedReadIntro, selectCompleted, selectReadIntro } from '../state/progress'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faArrowRight } from '@fortawesome/free-solid-svg-icons'
 import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'
 import { useContext, useEffect, useRef, useState } from 'react'
+import { GameHint, InteractiveGoalsWithHints } from './infoview/rpc_api'
+import Markdown from './markdown'
+import { useSelector } from 'react-redux'
+import { lastStepHasErrors } from './infoview/goals'
+
 import '../css/level.css'
 import '../css/chat.css'
 
@@ -18,33 +22,236 @@ function splitIntro (intro : string) {
   return intro.split(/\n(\s*\n)+/).filter(t => t.trim())
 }
 
-/** The buttons at the bottom of chat */
-export function ChatButtons () {
+/** Helper to check if a step has any hidden hints. */
+function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
+  return step?.goals[0]?.hints.some((hint) => hint.hidden)
+}
 
+/** Button which only appears if the current step has hidden hints that are not shown yet. */
+export function MoreHelpButton({selected=null} : {selected?: number}) {
+
+  const { t } = useTranslation()
+
+  const { proof } = React.useContext(ProofContext)
+  const { showHelp, setShowHelp } = React.useContext(ChatContext)
+
+  let k = proof?.steps.length ?
+    ((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected)
+    : 0
+
+  const activateHiddenHints = (ev) => {
+    // If the last step (`k`) has errors, we want the hidden hints from the
+    // second-to-last step to be affected
+    if (!(proof?.steps.length)) {return <></>}
+
+    // state must not be mutated, therefore we need to clone the set
+    let tmp = new Set(showHelp)
+    if (tmp.has(k)) {
+      tmp.delete(k)
+    } else {
+      tmp.add(k)
+    }
+    setShowHelp(tmp)
+    console.debug(`help: ${Array.from(tmp.values())}`)
+  }
+
+  if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
+    return <Button to="" onClick={activateHiddenHints}>
+      {t("Show more help!")}
+    </Button>
+  }
+}
+
+/** Placeholder that takes the same space as a button. */
+function ButtonPlaceholder() {
+  return <div className='btn-placeholder'/>
+}
+
+/** The buttons at the bottom of chat. */
+export function ChatButtons ({counter=undefined, setCounter=()=>{}, introMessages=[]} : {
+  counter?: number
+  setCounter?: React.Dispatch<React.SetStateAction<number>>
+  introMessages?: GameHintWithStep[]
+}) {
+
+  const { mobile } = useContext(PreferencesContext)
   const { gameId, worldId, levelId } = useContext(GameIdContext)
   const {setPage} = useContext(PageContext)
   const dispatch = useAppDispatch()
   const gameInfo = useGetGameInfoQuery({game: gameId})
 
+  const readIntro = useSelector(selectReadIntro(gameId, worldId))
+
   return <div className="button-row">
-    {(!worldId || !levelId) &&
+    {/* { ((mobile && !worldId) || worldId && !levelId) &&
       // Start button appears only on world selection and level 0.
       <Button className="btn"
           title=""
           to={worldId ? `/${gameId}/world/${worldId}/level/1` : ''}
           onClick={() => {
             if (!worldId) {
-              console.log('setting `openedIntro` to true')
+              console.log('setting `readIntro` to true')
               setPage(1)
-              dispatch(changedOpenedIntro({game: gameId, openedIntro: true}))
+              dispatch(changedReadIntro({game: gameId, readIntro: true}))
             }
           }} >
         Start&nbsp;<FontAwesomeIcon icon={faArrowRight}/>
       </Button>
-    }
+    } */}
+    {!levelId && (readIntro || (counter >= introMessages.length) ?
+      ((worldId || mobile) &&
+        <>
+          <ButtonPlaceholder />
+          <Button className="btn"
+              title=""
+              to={worldId ? `/${gameId}/world/${worldId}/level/1` : ''}
+              onClick={() => {
+                if (!worldId) {
+                  console.log('setting `readIntro` to true')
+                  setPage(1)
+                }
+              }} >
+            Start&nbsp;<FontAwesomeIcon icon={faArrowRight}/>
+          </Button>
+        </>
+      )
+      :
+      <>
+        <Button className="btn"
+            title=""
+            to=""
+            onClick={() => {
+              if (counter + 1 >= introMessages.length) {
+                dispatch(changedReadIntro({game: gameId, world: worldId, readIntro: true}))
+              }
+              setCounter(counter + 1)
+            }} >
+          {"Read"}
+        </Button>
+        <Button className="btn"
+            title=""
+            to=""
+            onClick={() => {
+              dispatch(changedReadIntro({game: gameId, world: worldId, readIntro: true}))
+              setCounter(introMessages.length)
+            }} >
+          Skip all
+        </Button>
+      </>
+
+    )}
+    { worldId && levelId && <MoreHelpButton /> }
   </div>
 }
 
+/** Insert the variable names in a hint. We do this client-side to prepare
+ * for i18n in the future. i.e. one should be able translate the `rawText`
+ * and have the variables substituted just before displaying.
+ */
+function getHintText(hint: GameHint): string {
+  const {gameId} = React.useContext(GameIdContext)
+  let { t } = useTranslation()
+  if (hint.rawText) {
+    // Replace the variable names used in the hint with the ones used by the player
+    // variable names are marked like `«{g}»` inside the text.
+    return t(hint.rawText, {ns: gameId}).replaceAll(/«\{(.*?)\}»/g, ((_, v) =>
+      // `hint.varNames` contains tuples `[oldName, newName]`
+      (hint.varNames.find(x => x[0] == v))[1]))
+  } else {
+    // hints created in the frontend do not have a `rawText`
+    // TODO: `hint.text` could be removed in theory.
+    return t(hint.text, {ns: gameId})
+  }
+}
+
+/** Bundling a hint with the proof-step it comes from. */
+type GameHintWithStep = {
+  hint: GameHint
+  step?: number
+  conclusion?: boolean
+}
+
+/** Filter hints to not show consequtive identical hints twice.
+ * Hidden hints are not filtered.
+ */
+export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
+  if (!hints) {
+    return []
+  } else if (!prevHints) {
+    return [...hints.filter((hint) => !hint.hidden), ...hints.filter((hint) => hint.hidden)]
+  } else {
+    return [...hints.filter((hint) => !hint.hidden &&
+      (prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)
+    ), ...hints.filter((hint) => hint.hidden)]
+  }
+}
+
+/** A hint as it is displayed in the chat. */
+export function Hint({hint, step=null, conclusion=false} : GameHintWithStep) {
+  const { levelId } = useContext(GameIdContext)
+  const { selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp } = useContext(ChatContext)
+
+  const { proof } = useContext(ProofContext)
+  const { typewriterMode } = useContext(PageContext)
+
+  function toggleSelection () {
+    if (!levelId) {return}
+
+    if (selectedStep !== null && selectedStep == step) {
+      setSelectedStep(undefined)
+    } else if (step < proof?.steps?.length) {
+      setSelectedStep(step)
+    }
+  }
+
+  // "Deleted hints" are marked in grey. They are used two-fold:
+  // In typewriter, deleting parts of the proof stores the removed hints as `deletedChat`
+  // until the next command is submitted; in editor, moving the cursor through the proof will
+  // render all hints
+  return <div className={`message ${conclusion ? 'success' : hint.hidden ? 'warning' : 'information'} step-${step}` +
+      ((selectedStep !== null && step == selectedStep) ? ' selected' : '') +
+      //
+      (!conclusion && step >= (typewriterMode ? proof?.steps?.length : selectedStep+1) ? ' deleted-hint' : '') } onClick={toggleSelection}>
+    <Markdown>{getHintText(hint)}</Markdown>
+  </div>
+}
+
+/** A collection of hints. If the `counter` is defined, only the first elements will be
+ * shown up to the value of the `counter`.
+ *
+ * Set `conclusion` to true to trigger different style and disable selecting/deleting.
+ */
+export function Hints({ hints, conclusion, counter=undefined } : {
+  hints: GameHintWithStep[],
+  conclusion?: boolean,
+  counter?: number
+}) {
+
+  const { showHelp } = useContext(ChatContext)
+
+  if (!hints) {
+    return <></>
+  }
+
+  // NOTE: This builds on the fact that `.slice(0, undefined)` returns the whole array!
+  // TODO: Should not use index as key.
+  return <>
+    { hints.slice(0, counter).map((hint, j) =>
+      ((!hint.hint.hidden || showHelp.has(hint.step)) &&
+        <Hint key={`hint-${hint.step}-${j}`} hint={hint.hint} step={hint.step} conclusion={conclusion} />
+      )
+    )}
+    {/* { //showHelp.has(hint.step) &&
+      hints.filter(hint => hint.hint.hidden).map((hint, j) =>
+      <Hint
+        key={`hidden-hint-${hint.step}-${j}`}
+        hint={hint.hint}
+        step={hint.step}
+        conclusion={hint.conclusion} />
+    )} */}
+  </>
+}
+
 /** the panel showing the game's introduction text */
 export function ChatPanel ({visible = true}) {
 
@@ -54,51 +261,100 @@ export function ChatPanel ({visible = true}) {
   const { mobile } = useContext(PreferencesContext)
   const { gameId, worldId, levelId } = useContext(GameIdContext)
 
+  const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
+
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
 
-  let [chatMessages, setChatMessages] = useState<Array<string>>([])
+  let [counter, setCounter] = useState(1)
+
+  let [introText, setIntroText] = useState<Array<GameHintWithStep>>([])
+  let [chatMessages, setChatMessages] = useState<Array<GameHintWithStep>>([])
+  let { deletedChat } = useContext(ChatContext)
+  let {proof} = useContext(ProofContext)
+
+  const readIntro = useSelector(selectReadIntro(gameId, worldId))
 
-  // Effect to clear chat and display the correct intro text
   useEffect(() => {
+    setCounter(1)
+  }, [gameId, worldId, levelId])
+
+  // load and display the correct intro text
+  useEffect(() => {
+    let messages: GameHintWithStep[] = []
+
     if (levelId > 0) {
+      let introText = t(levelInfo.data?.introduction, {ns : gameId}).trim()
+      let introHint: GameHintWithStep = {hint: {text: introText, hidden: false, rawText: introText }, step: 0}
+
       // playable level: show the level's intro
       if (levelInfo.data?.introduction) {
-        setChatMessages([t(levelInfo.data?.introduction, {ns : gameId})])
+        setIntroText([introHint])
+        // messages = messages.concat([introHint])
       }
       else {
-        setChatMessages([])
+        setIntroText([])
       }
+
+      proof?.steps?.forEach((step, i) => {
+        console.log("tesr")
+        messages = messages.concat(filterHints(step.goals[0]?.hints, proof.steps[i-1]?.goals[0]?.hints).map(hint => ({hint: hint, step: i})))
+      })
+
     } else {
       if (worldId) {
+        let introText = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).trim()
+        let introHints: GameHintWithStep[] = splitIntro(introText).map( txt => ({hint: {text: txt, hidden: false, rawText: txt }, step: 0}))
+
         // Level 0: show the world's intro
         if (gameInfo.data?.worlds.nodes[worldId].introduction) {
-          setChatMessages(splitIntro(t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId})))
+          // messages = messages.concat(introHints)
+          setIntroText(introHints)
         } else {
-          setChatMessages([])
+          setIntroText([])
         }
       } else {
+        let introText = t(gameInfo.data?.introduction, {ns : gameId}).trim()
+        let introHints: GameHintWithStep[] = splitIntro(introText).map( txt => ({hint: {text: txt, hidden: false, rawText: txt }, step: 0}))
+
         // world overview: show the game's intro
         if (gameInfo.data?.introduction) {
-          setChatMessages(splitIntro(t(gameInfo.data?.introduction, {ns : gameId})))
+          // messages = messages.concat(introHints)
+          setIntroText(introHints)
         } else {
-          setChatMessages([])
+          setIntroText([])
         }
       }
     }
-  }, [gameInfo, levelInfo, gameId, worldId, levelId])
+    console.log('chat messages:')
+    console.log(messages)
+    setChatMessages(messages)
+  }, [gameInfo, levelInfo, gameId, worldId, levelId, proof])
 
   return <div className={`column chat-panel${visible ? '' : ' hidden'}`}>
-    <div ref={chatRef} className="chat">
+    <div ref={chatRef} className="chat" >
+      <Hints hints={introText} counter={readIntro ? undefined : counter}/>
+      <Hints hints={chatMessages}/>
+      {/* {proof?.steps.map((step, i) =>
+        <Hints hints={step.goals[0]?.hints.map(hint => ({hint: hint, step: i}))}/>
+      )} */}
+      {/* <Hints hints={proof?.steps[proof?.steps?.length - 1]?.goals[0].hints.map(hint => ({hint: hint, step: proof?.steps?.length - 1}))} /> */}
 
-      {chatMessages.map(((t, i) =>
+      { deletedChat &&
+        <Hints hints={deletedChat.map(hint => ({hint: hint, step: proof?.steps?.length}))} />
+      }
+      { completed && levelInfo.data?.conclusion &&
+        <Hints hints={[{hint: {text: t("Level completed! 🎉"), rawText: t("Level completed! 🎉"), hidden: false}, step: proof?.steps?.length}, {hint: {text: levelInfo.data?.conclusion, rawText: levelInfo.data?.conclusion, hidden: false}, step: proof?.steps?.length} ]} conclusion={true} />
+      }
+
+      {/* {chatMessages.map(((t, i) =>
         t.trim() ?
           <Hint key={`intro-p-${i}`}
             hint={{text: t, hidden: false, rawText: t, varNames: []}}
-            step={0} selected={null} toggleSelection={undefined} />
+            step={0} />
         : <></>
-      ))}
+      ))} */}
     </div>
-    { mobile && <ChatButtons /> }
+    { <ChatButtons counter={counter} setCounter={setCounter} introMessages={introText}/> }
   </div>
 }

client/src/components/editor.tsx

@@ -0,0 +1,7 @@
+import * as React from 'react'
+
+export function Editor () {
+  return <p>
+    I'm an editor
+  </p>
+}

client/src/components/game.tsx

@@ -1,5 +1,5 @@
 import * as React from 'react'
-import { useEffect, useRef } from 'react'
+import { useContext, useEffect, useRef, useState } from 'react'
 import Split from 'react-split'
 import { Box, CircularProgress } from '@mui/material'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
@@ -7,10 +7,10 @@ import { faArrowRight } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
 import { useAppDispatch, useAppSelector } from '../hooks'
-import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
+import { changeTypewriterMode, changedReadIntro, changedSelection, codeEdited, selectCode, selectReadIntro, selectSelections, selectTypewriterMode } from '../state/progress'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api'
 import { Button } from './button'
-import { PageContext, PreferencesContext } from './infoview/context'
+import { ChatContext, PageContext, PreferencesContext, ProofContext } from './infoview/context'
 import { InventoryPanel } from './inventory'
 import { ErasePopup } from './popup/erase'
 import { InfoPopup } from './popup/info'
@@ -22,25 +22,25 @@ import { WorldTreePanel } from './world_tree'
 import '../css/game.css'
 import '../css/welcome.css'
 import '../css/level.css'
-import { Hint } from './hints'
 import i18next from 'i18next'
 import { useTranslation } from 'react-i18next'
 import { LoadingIcon } from './utils'
 import { ChatPanel } from './chat'
 import { DualEditor } from './infoview/main'
-import { Level } from './level'
+import { Level, LevelWrapper } from './level'
+import { GameHint, ProofState } from './infoview/rpc_api'
+import { useSelector } from 'react-redux'
+import { Diagnostic } from 'vscode-languageserver-types'
 
 /** main page of the game showing among others the tree of worlds/levels */
 function Game() {
 
-  const codeviewRef = useRef<HTMLDivElement>(null)
-
   const { gameId, worldId, levelId } = React.useContext(GameIdContext)
 
   // Load the namespace of the game
   i18next.loadNamespaces(gameId)
 
-  const {mobile} = React.useContext(PreferencesContext)
+  const {mobile} = useContext(PreferencesContext)
   const {isSavePreferences, language, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
 
   const gameInfo = useGetGameInfoQuery({game: gameId})
@@ -48,21 +48,35 @@ function Game() {
 
   const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
 
+  const {page, setPage} = useContext(PageContext)
 
-  const {page, setPage} = React.useContext(PageContext)
+  // TODO: recover `readIntro` functionality
 
-  // TODO: recover `openedIntro` functionality
+  // const [pageNumber, setPageNumber] = React.useState(readIntro ? 1 : 0)
 
-  // const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0)
+  // When deleting the proof, we want to keep to old messages around until
+  // a new proof has been entered. e.g. to consult messages coming from dead ends
+  const [deletedChat, setDeletedChat] = useState<Array<GameHint>>([])
+  // A set of row numbers where help is displayed
+  const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
+  // Select and highlight proof steps and corresponding hints
+  // TODO: with the new design, there is no difference between the introduction and
+  // a hint at the beginning of the proof...
+  const [selectedStep, setSelectedStep] = useState<number>(null)
 
-  // pop-ups
-  const [eraseMenu, setEraseMenu] = React.useState(false)
-  const [impressum, setImpressum] = React.useState(false)
-  const [privacy, setPrivacy] = React.useState(false)
-  const [info, setInfo] = React.useState(false)
-  const [rulesHelp, setRulesHelp] = React.useState(false)
-  const [uploadMenu, setUploadMenu] = React.useState(false)
-  const [preferencesPopup, setPreferencesPopup] = React.useState(false)
+  // The state variables for the `ProofContext`
+  const [proof, setProof] = useState<ProofState>({steps: [], diagnostics: [], completed: false, completedWithWarnings: false})
+  const [interimDiags, setInterimDiags] = useState<Array<Diagnostic>>([])
+  const [isCrashed, setIsCrashed] = useState<Boolean>(false)
+
+
+  const dispatch = useAppDispatch()
+
+  const typewriterMode = useSelector(selectTypewriterMode(gameId))
+  const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
+
+  const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
+  const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
 
   // set the window title
   useEffect(() => {
@@ -71,27 +85,40 @@ function Game() {
     }
   }, [gameInfo.data?.title])
 
-  return mobile ?
-    <div className="app-content mobile">
-      {<>
-        <ChatPanel visible={worldId ? (levelId == 0 && page == 1) :(page == 0)} />
-        { worldId ?
-          <Level visible={levelId > 0 && page == 1} /> :
-          <WorldTreePanel visible={page == 1} />
+  // Delete the current proof on changing level
+  useEffect(() => {
+    setProof(null)
+    setSelectedStep(null)
+    setDeletedChat([])
+    setShowHelp(new Set())
+  }, [gameId, worldId, levelId])
+
+  return <ChatContext.Provider value={{selectedStep, setSelectedStep, deletedChat, setDeletedChat, showHelp, setShowHelp}}>
+    <ProofContext.Provider value={{proof, setProof, interimDiags, setInterimDiags, crashed: isCrashed, setCrashed: setIsCrashed}}>
+    { mobile ?
+      <div className="app-content mobile">
+        {<>
+          <ChatPanel visible={worldId ? (levelId == 0 && page == 1) :(page == 0)} />
+          { worldId ?
+            (levelId > 0 && <LevelWrapper visible={page == 1} />) :
+            <WorldTreePanel visible={page == 1} />
+          }
+          <InventoryPanel visible={page == 2} />
+        </>
         }
-        <InventoryPanel visible={page == 2} />
-      </>
-      }
-    </div>
-  :
-    <Split className="app-content" minSize={0} snapOffset={200}  sizes={[25, 50, 25]}>
-      <ChatPanel />
-      <div>
-        {/* Note: apparently without this `div` the split panel bugs out. */}
-        {worldId ? <Level /> : <WorldTreePanel /> }
       </div>
-      <InventoryPanel />
-    </Split>
+    :
+      <Split className="app-content" minSize={0} snapOffset={200}  sizes={[25, 50, 25]}>
+        <ChatPanel />
+        <div className="column">
+          {/* Note: apparently without this `div` the split panel bugs out. */}
+          {worldId ? (levelId > 0 && <LevelWrapper />) : <WorldTreePanel /> }
+        </div>
+        <InventoryPanel />
+        </Split>
+    }
+    </ProofContext.Provider>
+  </ChatContext.Provider>
 
 }
 

client/src/components/hints.tsx

@@ -1,125 +0,0 @@
-import { GameHint, InteractiveGoalsWithHints, ProofState } from "./infoview/rpc_api";
-import * as React from 'react';
-import Markdown from './markdown';
-import { DeletedChatContext, ProofContext } from "./infoview/context";
-import { lastStepHasErrors } from "./infoview/goals";
-import { Button } from "./button";
-import { useTranslation } from "react-i18next";
-import { GameIdContext } from "../app";
-
-/** Plug-in the variable names in a hint. We do this client-side to prepare
- * for i18n in the future. i.e. one should be able translate the `rawText`
- * and have the variables substituted just before displaying.
- */
-function getHintText(hint: GameHint): string {
-  const {gameId} = React.useContext(GameIdContext)
-  let { t } = useTranslation()
-  if (hint.rawText) {
-    // Replace the variable names used in the hint with the ones used by the player
-    // variable names are marked like `«{g}»` inside the text.
-    return t(hint.rawText, {ns: gameId}).replaceAll(/«\{(.*?)\}»/g, ((_, v) =>
-      // `hint.varNames` contains tuples `[oldName, newName]`
-      (hint.varNames.find(x => x[0] == v))[1]))
-  } else {
-    // hints created in the frontend do not have a `rawText`
-    // TODO: `hint.text` could be removed in theory.
-    return t(hint.text, {ns: gameId})
-  }
-}
-
-export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
-  return <div className={`message information step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
-    <Markdown>{getHintText(hint)}</Markdown>
-  </div>
-}
-
-export function HiddenHint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
-  return <div className={`message warning step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
-    <Markdown>{getHintText(hint)}</Markdown>
-  </div>
-}
-
-export function Hints({hints, showHidden, step, selected, toggleSelection, lastLevel} : {hints: GameHint[], showHidden: boolean, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
-  if (!hints) {return <></>}
-  const openHints = hints.filter(hint => !hint.hidden)
-  const hiddenHints = hints.filter(hint => hint.hidden)
-
-  // TODO: Should not use index as key.
-  return <>
-    {openHints.map((hint, j) => <Hint key={`hint-${step}-${j}`} hint={hint} step={step} selected={selected} toggleSelection={toggleSelection} lastLevel={lastLevel} />)}
-    {showHidden && hiddenHints.map((hint, j) => <HiddenHint key={`hidden-hint-${step}-${j}`} hint={hint} step={step} selected={selected} toggleSelection={toggleSelection} lastLevel={lastLevel} />)}
-  </>
-}
-
-export function DeletedHint({hint} : {hint: GameHint}) {
-  return <div className="message information deleted-hint">
-    <Markdown>{getHintText(hint)}</Markdown>
-  </div>
-}
-
-export function DeletedHints({hints} : {hints: GameHint[]}) {
-
-  const openHints = hints.filter(hint => !hint.hidden)
-  const hiddenHints = hints.filter(hint => hint.hidden)
-
-  // TODO: Should not use index as key.
-  return <>
-    {openHints.map((hint, i) => <DeletedHint key={`deleted-hint-${i}`} hint={hint} />)}
-    {hiddenHints.map((hint, i) => <DeletedHint key={`deleted-hidden-hint-${i}`} hint={hint}/>)}
-  </>
-}
-
-/** Filter hints to not show consequtive identical hints twice.
- * Hidden hints are not filtered.
- */
-export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
-  if (!hints) {
-    return []}
-  else if (!prevHints) {
-    return hints }
-  else {
-    return hints.filter((hint) => hint.hidden ||
-    (prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)
-    )
-  }
-}
-
-
-function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
-  return step?.goals[0]?.hints.some((hint) => hint.hidden)
-}
-
-
-export function MoreHelpButton({selected=null} : {selected?: number}) {
-
-  const { t } = useTranslation()
-
-  const {proof, setProof} = React.useContext(ProofContext)
-  const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)
-
-  let k = proof?.steps.length ?
-    ((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected)
-    : 0
-
-  const activateHiddenHints = (ev) => {
-    // If the last step (`k`) has errors, we want the hidden hints from the
-    // second-to-last step to be affected
-    if (!(proof?.steps.length)) {return}
-
-    // state must not be mutated, therefore we need to clone the set
-    let tmp = new Set(showHelp)
-    if (tmp.has(k)) {
-      tmp.delete(k)
-    } else {
-      tmp.add(k)
-    }
-    setShowHelp(tmp)
-    console.debug(`help: ${Array.from(tmp.values())}`)
-  }
-
-  if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
-    return <Button to="" onClick={activateHiddenHints}>
-      {t("Show more help!")}
-    </Button>
-  }
-}

client/src/components/infoview/context.ts

@@ -93,30 +93,17 @@ export const PreferencesContext = React.createContext<IPreferencesContext>({
   setLanguage: () => {},
 })
 
-export const WorldLevelIdContext = React.createContext<{
-  worldId : string,
-  levelId: number
-}>({
-  worldId : null,
-  levelId: 0,
-})
 
-/** Context to keep highlight selected proof step and corresponding chat messages. */
-export const SelectionContext = React.createContext<{
+export const ChatContext = React.createContext<{
   selectedStep : number,
   setSelectedStep: React.Dispatch<React.SetStateAction<number>>
-}>({
-  selectedStep : undefined,
-  setSelectedStep: () => {}
-})
-
-/** Context for deleted Hints that are visible just a bit after they've been deleted */
-export const DeletedChatContext = React.createContext<{
   deletedChat : GameHint[],
   setDeletedChat: React.Dispatch<React.SetStateAction<Array<GameHint>>>
   showHelp : Set<number>,
   setShowHelp: React.Dispatch<React.SetStateAction<Set<number>>>
 }>({
+  selectedStep : undefined,
+  setSelectedStep: () => {},
   deletedChat: undefined,
   setDeletedChat: () => {},
   showHelp: undefined,

client/src/components/infoview/main.tsx

@@ -20,25 +20,26 @@ import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 
 import { GameIdContext } from '../../app';
 import { useAppDispatch, useAppSelector } from '../../hooks';
-import { LevelInfo, useGetGameInfoQuery } from '../../state/api';
+import { LevelInfo, useGetGameInfoQuery, useLoadLevelQuery } from '../../state/api';
 import { changedInventory, levelCompleted, selectCode, selectCompleted, selectInventory } from '../../state/progress';
 import Markdown from '../markdown';
 
 import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
 import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals';
-import { DeletedChatContext, PageContext, PreferencesContext, MonacoEditorContext, ProofContext, SelectionContext, WorldLevelIdContext } from './context';
+import { ChatContext, PageContext, PreferencesContext, MonacoEditorContext, ProofContext } from './context';
 import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter';
 import { InteractiveDiagnostic } from '@leanprover/infoview/*';
 import { Button } from '../button';
 import { CircularProgress } from '@mui/material';
 import { GameHint, InteractiveGoalsWithHints, ProofState } from './rpc_api';
 import { store } from '../../state/store';
-import { Hints, MoreHelpButton, filterHints } from '../hints';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { DiagnosticSeverity } from 'vscode-languageclient';
 import { useTranslation } from 'react-i18next';
 import path from 'path';
+import { useContext } from 'react';
+import { Hints, MoreHelpButton, filterHints } from '../chat';
 
 
 /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
@@ -49,7 +50,7 @@ export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize })
   const { typewriterMode, lockEditorMode } = React.useContext(PageContext)
   return <>
     <div className={(typewriterMode && !lockEditorMode) ? 'hidden' : ''}>
-      <ExerciseStatement data={level} showLeanStatement={true} />
+      {/* <ExerciseStatement showLeanStatement={true} /> */}
       <div ref={codeviewRef} className={'codeview'}></div>
     </div>
     {ec ?
@@ -135,23 +136,24 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
  *
  * If `showLeanStatement` is true, it will additionally display the lean code.
  */
-function ExerciseStatement({ data, showLeanStatement = false }) {
+export function ExerciseStatement({ showLeanStatement = false }) {
   let { t } = useTranslation()
-  const {gameId} = React.useContext(GameIdContext)
+  const {gameId, worldId, levelId } = React.useContext(GameIdContext)
+  const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
 
-  if (!(data?.descrText || data?.descrFormat)) { return <></> }
+  if (!(levelInfo.data?.descrText || levelInfo.data?.descrFormat)) { return <></> }
   return <>
     <div className="exercise-statement">
-      {data?.descrText ?
+      {levelInfo.data?.descrText ?
         <Markdown>
-          {(data?.displayName ? `**${t("Theorem")}** \`${data?.displayName}\`: ` : '') + t(data?.descrText, {ns: gameId})}
-        </Markdown> : data?.displayName &&
+          {(levelInfo.data?.displayName ? `**${t("Theorem")}** \`${levelInfo.data?.displayName}\`: ` : '') + t(levelInfo.data?.descrText, {ns: gameId})}
+        </Markdown> : levelInfo.data?.displayName &&
         <Markdown>
-          {`**${t("Theorem")}** \`${data?.displayName}\``}
+          {`**${t("Theorem")}** \`${levelInfo.data?.displayName}\``}
         </Markdown>
       }
-      {data?.descrFormat && showLeanStatement &&
-        <p><code className="lean-code">{data?.descrFormat}</code></p>
+      {levelInfo.data?.descrFormat && showLeanStatement &&
+        <p><code className="lean-code">{levelInfo.data?.descrFormat}</code></p>
       }
     </div>
   </>
@@ -162,13 +164,10 @@ function ExerciseStatement({ data, showLeanStatement = false }) {
 export function Main(props: { world: string, level: number, data: LevelInfo}) {
   let { t } = useTranslation()
   const ec = React.useContext(EditorContext);
-  const {gameId} = React.useContext(GameIdContext)
-  const {worldId, levelId} = React.useContext(WorldLevelIdContext)
+  const {gameId, worldId, levelId} = React.useContext(GameIdContext)
 
   const { proof, setProof } = React.useContext(ProofContext)
-  const {selectedStep, setSelectedStep} = React.useContext(SelectionContext)
-  const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
-
+  const {selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp} = React.useContext(ChatContext)
 
   function toggleSelection(line: number) {
     return (ev) => {
@@ -249,11 +248,11 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
         </div>
       }
       <Infos />
-      <Hints hints={proof?.steps[curPos?.line]?.goals[0]?.hints}
+      {/* <Hints hints={proof?.steps[curPos?.line]?.goals[0]?.hints}
         showHidden={showHelp.has(curPos?.line)} step={curPos?.line}
         selected={selectedStep} toggleSelection={toggleSelection(curPos?.line)}
         lastLevel={curPos?.line == proof?.steps.length - 1}/>
-      <MoreHelpButton selected={curPos?.line}/>
+      <MoreHelpButton selected={curPos?.line}/> */}
     </div>
   }
 
@@ -403,23 +402,21 @@ export function TypewriterInterfaceWrapper(props: { world: string, level: number
 export function TypewriterInterface({props}) {
   let { t } = useTranslation()
   const ec = React.useContext(EditorContext)
-  const {gameId} = React.useContext(GameIdContext)
+  const {gameId,worldId, levelId} = React.useContext(GameIdContext)
   const editor = React.useContext(MonacoEditorContext)
   const model = editor.getModel()
   const uri = model.uri.toString()
 
   const gameInfo = useGetGameInfoQuery({game: gameId})
-  const {worldId, levelId} = React.useContext(WorldLevelIdContext)
   let image: string = gameInfo.data?.worlds.nodes[worldId].image
 
 
   const [disableInput, setDisableInput] = React.useState<boolean>(false)
   const [loadingProgress, setLoadingProgress] = React.useState<number>(0)
-  const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
+  const { selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp } = React.useContext(ChatContext)
   const {mobile} = React.useContext(PreferencesContext)
   const { proof, setProof, crashed, setCrashed, interimDiags } = React.useContext(ProofContext)
   const { setTypewriterInput } = React.useContext(PageContext)
-  const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
 
   const proofPanelRef = React.useRef<HTMLDivElement>(null)
   // const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
@@ -513,19 +510,19 @@ export function TypewriterInterface({props}) {
   return <div className="typewriter-interface">
     <RpcContext.Provider value={rpcSess}>
     <div className="content">
-      <div className='world-image-container empty'>
+      {/* <div className='world-image-container empty'>
         {image &&
           <img className="contain" src={path.join("data", gameId, image)} alt="" />
         }
 
-      </div>
-      <div className="tmp-pusher">
-        {/* <div className="world-image-container empty">
+      </div> */}
+      {/* <div className="tmp-pusher">
+        <div className="world-image-container empty">
 
-        </div> */}
-      </div>
+        </div>
+      </div> */}
       <div className='proof' ref={proofPanelRef}>
-        <ExerciseStatement data={props.data} />
+        {/* <ExerciseStatement /> */}
         {crashed ? <div>
           <p className="crashed_message">{t("Crashed! Go to editor mode and fix your proof! Last server response:")}</p>
           {interimDiags.map(diag => {
@@ -569,8 +566,7 @@ export function TypewriterInterface({props}) {
                   }
                   {mobile &&
                     <Hints key={`hints-${i}`}
-                      hints={filteredHints} showHidden={showHelp.has(i)} step={i}
-                      selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
+                      hints={filteredHints.map(hint => ({hint: hint, step: i}))} />
                   }
                   {/* <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
                   {!(isLastStepWithErrors(proof, i)) &&

client/src/components/infoview/rpc_api.ts

@@ -50,7 +50,7 @@ export interface GameHint {
   text: string;
   hidden: boolean;
   rawText: string;
-  varNames: string[][]; // in Lean: `Array (Name × Name)`
+  varNames?: string[][]; // in Lean: `Array (Name × Name)`
 }
 
 export interface InteractiveGoalWithHints {

client/src/components/infoview/typewriter.tsx

@@ -17,10 +17,11 @@ import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } fro
 import { Diagnostic } from 'vscode-languageserver-types';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
-import { DeletedChatContext, PageContext, MonacoEditorContext, ProofContext } from './context'
+import { ChatContext, PageContext, MonacoEditorContext, ProofContext } from './context'
 import { goalsToString, lastStepHasErrors, loadGoals } from './goals'
 import { GameHint, ProofState } from './rpc_api'
 import { useTranslation } from 'react-i18next'
+import { GameIdContext } from '../../app'
 
 export interface GameDiagnosticsParams {
   uri: DocumentUri;
@@ -81,8 +82,8 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
 
   /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
-  const model = editor.getModel()
-  const uri = model.uri.toString()
+  const model = editor?.getModel()
+  const uri = model?.uri.toString()
 
   const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
   const [processing, setProcessing] = useState(false)
@@ -94,8 +95,10 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
   // The context storing all information about the current proof
   const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext)
 
+  const {gameId, worldId, levelId} = React.useContext(GameIdContext)
+
   // state to store the last batch of deleted messages
-  const {setDeletedChat} = React.useContext(DeletedChatContext)
+  const {setDeletedChat} = React.useContext(ChatContext)
 
   const rpcSess = React.useContext(RpcContext)
 
@@ -106,13 +109,13 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
     // TODO: Desired logic is to only reset this after a new *error-free* command has been entered
     setDeletedChat([])
 
-    const pos = editor.getPosition()
+    const pos = editor?.getPosition()
     if (typewriterInput) {
       setProcessing(true)
-      editor.executeEdits("typewriter", [{
+      editor?.executeEdits("typewriter", [{
         range: monaco.Selection.fromPositions(
           pos,
-          editor.getModel().getFullModelRange().getEndPosition()
+          editor?.getModel()?.getFullModelRange()?.getEndPosition()
         ),
         text: typewriterInput.trim() + "\n",
         forceMoveMarkers: false
@@ -122,7 +125,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
       loadGoals(rpcSess, uri, setProof, setCrashed)
     }
 
-    editor.setPosition(pos)
+    editor?.setPosition(pos)
   }, [typewriterInput, editor])
 
   useEffect(() => {
@@ -133,8 +136,9 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
 
   /* Load proof on start/switching to typewriter */
   useEffect(() => {
+    setProof(null)
     loadGoals(rpcSess, uri, setProof, setCrashed)
-  }, [])
+  }, [gameId, worldId, levelId])
 
   /** If the last step has an error, add the command to the typewriter. */
   useEffect(() => {
@@ -157,7 +161,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
       // TODO: loadAllGoals()
       if (!hasErrors(params.diagnostics)) {
         //setTypewriterInput("")
-        editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
+        editor?.setPosition(editor?.getModel()?.getFullModelRange()?.getEndPosition())
       }
     } else {
       // console.debug(`expected uri: ${uri}, got: ${params.uri}`)

client/src/components/inventory.tsx

@@ -12,7 +12,6 @@ import { store } from '../state/store';
 import { useSelector } from 'react-redux';
 import { useTranslation } from 'react-i18next';
 import { t } from 'i18next';
-import { WorldLevelIdContext } from './infoview/context';
 import { NavButton } from './navigation';
 import { LoadingIcon } from './utils';
 
@@ -37,16 +36,24 @@ const InventoryContext = createContext<{
 
 /**
  */
-function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, recent=false }) {
+function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc } :
+    { item: InventoryTile,
+      name: any,
+      displayName: any,
+      locked: any,
+      disabled: any,
+      newly: any,
+      showDoc: any
+    }) {
   const icon = locked ? <FontAwesomeIcon icon={faLock} /> :
-               disabled ? <FontAwesomeIcon icon={faBan} /> : item.st
+               disabled ? <FontAwesomeIcon icon={faBan} /> : <></>
   const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : ""
   // Note: This is somewhat a hack as the statement of lemmas comes currently in the form
   // `Namespace.statement_name (x y : Nat) : some type`
   const title = locked ? t("Not unlocked yet") :
                 disabled ? t("Not available in this level") : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
 
-  const { gameId } = React.useContext(GameIdContext)
+  const { gameId, worldId, levelId } = React.useContext(GameIdContext)
   const difficulty = useSelector(selectDifficulty(gameId))
 
   // local state to show checkmark after pressing the copy button
@@ -67,7 +74,10 @@ function InventoryItem({item, name, displayName, locked, disabled, newly, showDo
     ev.stopPropagation()
   }
 
-  return <div className={`item ${className}${(difficulty == 0) ? ' enabled' : ''}${recent ? ' recent' : ''}`} onClick={handleClick} title={title}>
+  return <div className={`item ${className}` +
+      `${(difficulty == 0) ? ' enabled' : ''}` +
+      `${item.world == worldId && item.level == levelId - 1 ? ' recent' : ''}` +
+      `${item.world == worldId && item.level < levelId ? ' current-world' : ''}` } onClick={handleClick} title={title}>
     {icon} {displayName}
     <div className="copy-button" onClick={copyItemName}>
       {copied ? <FontAwesomeIcon icon={faCheck} /> : <FontAwesomeIcon icon={faClipboard} />}
@@ -92,7 +102,7 @@ function InventoryList({ items, tab=null, setTab=()=>{} } :
 
   const [categories, setCategories] = useState<Array<string>>([])
   const [modifiedItems, setModifiedItems] = useState<Array<InventoryTile>>([])
-  const [recentItems, setRecentItems] = useState<Array<InventoryTile>>([])
+  const [currentWorldItems, setCurrentWorldItems] = useState<Array<InventoryTile>>([])
 
 
   useEffect(() => {
@@ -111,7 +121,8 @@ function InventoryList({ items, tab=null, setTab=()=>{} } :
     let _modifiedItems : InventoryTile[] = items?.map(tile => inventory.includes(tile.name) ? {...tile, locked: false} : tile)
     setModifiedItems(_modifiedItems)
     // Item(s) proved in the preceeding level
-    setRecentItems(_modifiedItems.filter(x => x.world == worldId && x.level == levelId - 1))
+    setCurrentWorldItems(_modifiedItems.filter(x => x.world == worldId && x.level < levelId))
+    // setRecentItems(_modifiedItems.filter(x => x.world == worldId && x.level == levelId - 1))
 
   }, [items, inventory])
 
@@ -120,7 +131,7 @@ function InventoryList({ items, tab=null, setTab=()=>{} } :
       <div className="tab-bar">
         {categories.map((cat) => {
           let hasNew = modifiedItems.filter(item => item.new && (cat == item.category)).length > 0
-          return <div key={`category-${cat}`} className={`tab${cat == (tab ?? categories[0]) ? " active": ""}${hasNew ? ' new': ''}${recentItems.map(x => x.category).includes(cat) ? ' recent': ''}`}
+          return <div key={`category-${cat}`} className={`tab${cat == (tab ?? categories[0]) ? " active": ""}${hasNew ? ' new': ''}${currentWorldItems.map(x => x.category).includes(cat) ? ' recent': ''}`}
             onClick={() => { setTab(cat) }}>{cat}</div>})}
       </div>}
     <div className="inventory-list">
@@ -134,7 +145,6 @@ function InventoryList({ items, tab=null, setTab=()=>{} } :
               showDoc={() => {setDocTile(item)}}
               name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false}
               disabled={item.disabled}
-              recent={recentItems.map(x => x.name).includes(item.name)}
               newly={item.new} />
         })
       }
@@ -155,7 +165,6 @@ export function Inventory () {
 
   /** Helper function to find if a list of tiles comprises any new elements. */
   function containsNew(tiles: InventoryTile[]) {
-    console.log(tiles)
     return tiles?.filter(item => item.new).length > 0
   }
 

client/src/components/landing_page.tsx

@@ -59,7 +59,7 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
 
         <td>
           {data.languages.map((lang) => (
-            <Flag iso={lang} showTitle={true} />
+            <Flag key={lang} iso={lang} showTitle={true} />
           ))}
         </td>
       </tr>

client/src/components/level.tsx

@@ -4,7 +4,7 @@ import { useSelector, useStore } from 'react-redux'
 import Split from 'react-split'
 import { useParams } from 'react-router-dom'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faHome, faArrowRight } from '@fortawesome/free-solid-svg-icons'
+import { faHome, faArrowRight, faCode, faTerminal } from '@fortawesome/free-solid-svg-icons'
 import { CircularProgress } from '@mui/material'
 import type { Location } from 'vscode-languageserver-protocol'
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
@@ -17,6 +17,7 @@ import { EditorContext } from '../../../node_modules/lean4-infoview/src/infoview
 import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-infoview/src/infoview/editorConnection'
 import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event'
 import { Diagnostic } from 'vscode-languageserver-types'
+import { DiagnosticSeverity } from 'vscode-languageclient';
 
 import { GameIdContext } from '../app'
 import { useAppDispatch, useAppSelector } from '../hooks'
@@ -27,12 +28,13 @@ import { store } from '../state/store'
 import { Button } from './button'
 import Markdown from './markdown'
 import {InventoryPanel} from './inventory'
-import { hasInteractiveErrors } from './infoview/typewriter'
-import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
-  ProofContext, SelectionContext, WorldLevelIdContext, PageContext } from './infoview/context'
-import { DualEditor } from './infoview/main'
+import { Editor } from './editor'
+import { Typewriter } from './typewriter'
+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, Hint, Hints, MoreHelpButton, filterHints } from './hints'
+import { DeletedHints, Hints, MoreHelpButton } from './hints'
 import path from 'path';
 
 import '@fontsource/roboto/300.css'
@@ -54,14 +56,14 @@ import { PreferencesPopup } from './popup/preferences'
 import { useTranslation } from 'react-i18next'
 import i18next from 'i18next'
 import { ChatButtons } from './chat'
+import { NavButton } from './navigation'
 
 
 monacoSetup()
 
 export function Level({visible = true}) {
-  // const params = useParams()
-  // const levelId = parseInt(params.levelId)
-  // const worldId = params.worldId
+  let { t } = useTranslation()
+
 
   const {gameId, worldId, levelId} = React.useContext(GameIdContext)
 
@@ -71,153 +73,9 @@ export function Level({visible = true}) {
   })
 
   const gameInfo = useGetGameInfoQuery({game: gameId})
+  const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
 
-  // pop-ups
-  const [impressum, setImpressum] = React.useState(false)
-  const [privacy, setPrivacy] = React.useState(false)
-  const [info, setInfo] = React.useState(false)
-  const [preferencesPopup, setPreferencesPopup] = React.useState(false)
-
-  function closeImpressum()   {setImpressum(false)}
-  function closePrivacy()   {setPrivacy(false)}
-  function closeInfo()        {setInfo(false)}
-  function closePreferencesPopup() {setPreferencesPopup(false)}
-  function toggleImpressum()  {setImpressum(!impressum)}
-  function toggleInfo()       {setInfo(!info)}
-  function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)}
-
-  useEffect(() => {}, [])
-
-  return <div className={visible?'':'hidden'}>
-    <WorldLevelIdContext.Provider value={{worldId, levelId}} >
-      <PlayableLevel key={`${worldId}/${levelId}`} />
-    </WorldLevelIdContext.Provider>
-  </div>
-}
-
-function ChatPanel({lastLevel, visible = true}) {
-  let { t } = useTranslation()
-  const chatRef = useRef<HTMLDivElement>(null)
-  const {mobile} = useContext(PreferencesContext)
-  const {gameId} = useContext(GameIdContext)
-  const {worldId, levelId} = useContext(WorldLevelIdContext)
-  const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
-  const {proof, setProof} = useContext(ProofContext)
-  const {deletedChat, setDeletedChat, showHelp, setShowHelp} = useContext(DeletedChatContext)
-  const {selectedStep, setSelectedStep} = useContext(SelectionContext)
-  const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
-
-  let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
-
-  function toggleSelection(line: number) {
-    return (ev) => {
-      console.debug('toggled selection')
-      if (selectedStep == line) {
-        setSelectedStep(undefined)
-      } else {
-        setSelectedStep(line)
-      }
-    }
-  }
-
-  useEffect(() => {
-    // TODO: For some reason this is always called twice
-    console.debug('scroll chat')
-    if (!mobile) {
-      chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0)
-    }
-  }, [proof, showHelp])
-
-  // Scroll to element if selection changes
-  useEffect(() => {
-    if (typeof selectedStep !== 'undefined') {
-      Array.from(chatRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => {
-        elem.scrollIntoView({block: "center"})
-      })
-    }
-  }, [selectedStep])
-
-  // useEffect(() => {
-  //   // // Scroll to top when loading a new level
-  //   // // TODO: Thats the wrong behaviour probably
-  //   // chatRef.current!.scrollTo(0,0)
-  // }, [gameId, worldId, levelId])
-
-  let introText: Array<string> = t(level?.data?.introduction, {ns: gameId}).split(/\n(\s*\n)+/)
-
-  return <div className={`chat-panel ${visible ? '' : 'hidden'}`}>
-    <div ref={chatRef} className="chat">
-      {introText?.filter(t => t.trim()).map(((t, i) =>
-        // Show the level's intro text as hints, too
-        <Hint key={`intro-p-${i}`}
-          hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
-      ))}
-      {proof?.steps.map((step, i) => {
-        let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
-        if (step.goals.length > 0 && !isLastStepWithErrors(proof, i)) {
-          return <Hints key={`hints-${i}`}
-          hints={filteredHints} showHidden={showHelp.has(i)} step={i}
-          selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
-        }
-      })}
-
-      {/* {modifiedHints.map((step, i) => {
-        // It the last step has errors, it will have the same hints
-        // as the second-to-last step. Therefore we should not display them.
-        if (!(i == proof?.steps.length - 1 && withErr)) {
-          // TODO: Should not use index as key.
-          return <Hints key={`hints-${i}`}
-            hints={step} showHidden={showHelp.has(i)} step={i}
-            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
-        }
-      })} */}
-      <DeletedHints hints={deletedChat}/>
-      {proof?.completed &&
-        <>
-          <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
-            {t("Level completed! 🎉")}
-          </div>
-          {level?.data?.conclusion?.trim() &&
-            <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
-              <Markdown>{t(level?.data?.conclusion, {ns: gameId})}</Markdown>
-            </div>
-          }
-        </>
-      }
-    </div>
-    <div className="button-row">
-      {proof?.completed && (lastLevel ?
-        <Button to={`/${gameId}`}>
-          <FontAwesomeIcon icon={faHome} />&nbsp;{t("Leave World")}
-        </Button> :
-        <Button to={`/${gameId}/world/${worldId}/level/${levelId + 1}`}>
-          {t("Next")}&nbsp;<FontAwesomeIcon icon={faArrowRight} />
-        </Button>)
-        }
-      <MoreHelpButton />
-    </div>
-  </div>
-}
-
-
-export function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject<HTMLDivElement>, visible?: boolean}) {
-  const {gameId} = React.useContext(GameIdContext)
-  const {worldId, levelId} = useContext(WorldLevelIdContext)
-  const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
-  const gameInfo = useGetGameInfoQuery({game: gameId})
-  return <div className={`exercise-panel ${visible ? '' : 'hidden'}`}>
-    <div className="exercise">
-      <DualEditor level={level?.data} codeviewRef={codeviewRef} levelId={levelId} worldId={worldId} worldSize={gameInfo.data?.worldSize[worldId]}/>
-    </div>
-  </div>
-}
-
-export function PlayableLevel() {
-  let { t } = useTranslation()
   const codeviewRef = useRef<HTMLDivElement>(null)
-  const {gameId} = React.useContext(GameIdContext)
-  const {worldId, levelId} = useContext(WorldLevelIdContext)
-  const {mobile} = React.useContext(PreferencesContext)
 
   const dispatch = useAppDispatch()
 
@@ -227,20 +85,9 @@ export function PlayableLevel() {
   const typewriterMode = useSelector(selectTypewriterMode(gameId))
   const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
 
-  const gameInfo = useGetGameInfoQuery({game: gameId})
-  const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
+  const {deletedChat, setDeletedChat,showHelp, setShowHelp} = useContext(ChatContext)
+  const {proof, setProof} = useContext(ProofContext)
 
-  // The state variables for the `ProofContext`
-  const [proof, setProof] = useState<ProofState>({steps: [], diagnostics: [], completed: false, completedWithWarnings: false})
-  const [interimDiags, setInterimDiags] = useState<Array<Diagnostic>>([])
-  const [isCrashed, setIsCrashed] = useState<Boolean>(false)
-
-
-  // When deleting the proof, we want to keep to old messages around until
-  // a new proof has been entered. e.g. to consult messages coming from dead ends
-  const [deletedChat, setDeletedChat] = useState<Array<GameHint>>([])
-  // A set of row numbers where help is displayed
-  const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
   // Only for mobile layout
   const {page, setPage} = useContext(PageContext)
 
@@ -259,8 +106,6 @@ export function PlayableLevel() {
   const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
   function closeInventoryDoc () {setInventoryDoc(null)}
 
-
-
   const onDidChangeContent = (code) => {
     dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code}))
   }
@@ -309,7 +154,7 @@ export function PlayableLevel() {
 
   useEffect (() => {
     // Lock editor mode
-    if (level?.data?.template) {
+    if (levelInfo.data?.template) {
       setLockEditorMode(true)
 
       if (editor) {
@@ -325,12 +170,12 @@ export function PlayableLevel() {
         // TODO: It does seem that the template is always indented by spaces.
         // This is a hack, assuming there are exactly two.
         if (!code.join('').trim().length) {
-          console.debug(`inserting template:\n${level.data.template}`)
+          console.debug(`inserting template:\n${levelInfo.data.template}`)
           // TODO: This does not work! HERE
           // Probably overwritten by a query to the server
           editor.executeEdits("template-writer", [{
             range: editor.getModel().getFullModelRange(),
-            text: level.data.template + `\n`,
+            text: levelInfo.data.template + `\n`,
             forceMoveMarkers: true
           }])
         } else {
@@ -340,7 +185,7 @@ export function PlayableLevel() {
     } else {
       setLockEditorMode(false)
     }
-  }, [level, levelId, worldId, gameId, editor])
+  }, [levelInfo, levelId, worldId, gameId, editor])
 
 
   useEffect(() => {
@@ -407,103 +252,345 @@ export function PlayableLevel() {
     }
   }, [editor, typewriterMode, lockEditorMode, onigasmH == null])
 
-  return <>
-    <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
-    <DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
-      <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
-        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockEditorMode, setLockEditorMode}}>
-          <ProofContext.Provider value={{proof, setProof, interimDiags, setInterimDiags, crashed: isCrashed, setCrashed: setIsCrashed}}>
-            <EditorContext.Provider value={editorConnection}>
-              <MonacoEditorContext.Provider value={editor}>
-                {/* <LevelAppBar
-                  pageNumber={page} setPageNumber={setPage}
-                  isLoading={level.isLoading}
-                  levelTitle={(mobile ? "" : t("Level")) + ` ${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
-                    (level?.data?.title && ` : ${t(level?.data?.title, {ns: gameId})}`)}
-                    toggleImpressum={toggleImpressum}
-                    togglePrivacy={togglePrivacy}
-                    toggleInfo={toggleInfo}
-                  togglePreferencesPopup={togglePreferencesPopup}
-                  /> */}
-                <ExercisePanel codeviewRef={codeviewRef} />
-              </MonacoEditorContext.Provider>
-            </EditorContext.Provider>
-          </ProofContext.Provider>
-        </InputModeContext.Provider>
-      </SelectionContext.Provider>
-    </DeletedChatContext.Provider>
-  </>
+
+  return <div className={visible?'':'hidden'}>
+      {/* <div style={levelInfo.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div> */}
+              <EditorContext.Provider value={editorConnection}>
+                <MonacoEditorContext.Provider value={editor}>
+                    {levelId > 0 &&
+                    <ExercisePanel codeviewRef={codeviewRef} />}
+                </MonacoEditorContext.Provider>
+              </EditorContext.Provider>
+  </div>
 }
 
+export function LevelWrapper({visible = true}) {
+  let { t } = useTranslation()
+  const {gameId, worldId, levelId} = React.useContext(GameIdContext)
+
+  // Load the namespace of the game
+  i18next.loadNamespaces(gameId).catch(err => {
+    console.warn(`translations for ${gameId} do not exist.`)
+  })
+
+
+  const { mobile } = useContext(PreferencesContext)
+
+  const gameInfo = useGetGameInfoQuery({game: gameId})
+  const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
+
+  let image: string = gameInfo.data?.worlds.nodes[worldId].image
+
+  const codeviewRef = useRef<HTMLDivElement>(null)
+  const proofPanelRef = React.useRef<HTMLDivElement>(null)
+
+  // set to true to prevent switching between typewriter and editor
+  const [lockEditorMode, setLockEditorMode] = useState(false)
+  const [typewriterInput, setTypewriterInput] = useState("")
+  const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
+
+  // // impressum pop-up
+  // function toggleImpressum() {setImpressum(!impressum)}
+  // function togglePrivacy() {setPrivacy(!privacy)}
+
+  // When clicking on an inventory item, the inventory is overlayed by the item's doc.
+  // If this state is set to a pair `(name, type)` then the according doc will be open.
+  // Set `inventoryDoc` to `null` to close the doc
+  const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
+  function closeInventoryDoc () {setInventoryDoc(null)}
+
+
+
+  const dispatch = useAppDispatch()
+
+  const typewriterMode = useSelector(selectTypewriterMode(gameId))
+  const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
+
+  const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
+  const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
+
+
+  const onDidChangeContent = (code) => {
+    dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code}))
+  }
+
+  const onDidChangeSelection = (monacoSelections) => {
+    const selections = monacoSelections.map(
+      ({selectionStartLineNumber, selectionStartColumn, positionLineNumber, positionColumn}) =>
+      {return {selectionStartLineNumber, selectionStartColumn, positionLineNumber, positionColumn}})
+    dispatch(changedSelection({game: gameId, world: worldId, level: levelId, selections}))
+  }
+
+
+  useEffect(() => {
+    console.info(`Loading Level: ${mobile}`)
+  }, [mobile, gameId, worldId, levelId])
+
+  // const {editor, infoProvider, editorConnection} =
+  // useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection)
+
+
+
+  /** toggle input mode if allowed */
+  function toggleInputMode(ev: React.MouseEvent) {
+    if (!lockEditorMode) {
+      setTypewriterMode(!typewriterMode)
+      console.log('test')
+    }
+  }
+
+  // { typewriterMode ? <Typewriter /> : <Editor /> }
+
+  // <EditorContext.Provider value={editorConnection}>
+  // <MonacoEditorContext.Provider value={editor}>
+  return <div className="exercise">
+      { image &&
+        <div className='world-image'>
+          <img className="contain" src={path.join("data", gameId, image)} alt="" />
+        </div>
+      }
+      { levelId > 0 &&
+        <div className="exercise-content">
+            <NavButton
+              className="btn-input-mode"
+              icon={(typewriterMode && !lockEditorMode) ? faCode : faTerminal}
+              inverted={true}
+              disabled={levelId == 0 || lockEditorMode}
+              onClick={(ev) => toggleInputMode(ev)}
+              title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")} />
+          <div className="tmp-pusher" />
+          <div className='proof' ref={proofPanelRef}>
+            <ExerciseStatement showLeanStatement={!typewriterMode} />
+            <Level/>
+            {/* { typewriterMode ? <Typewriter /> : <Editor /> } */}
+          </div>
+
+        </div>
+      }
+
+    </div>
+}
+
+// </MonacoEditorContext.Provider>
+// </EditorContext.Provider>
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+// function ChatPanel({lastLevel, visible = true}) {
+//   let { t } = useTranslation()
+//   const chatRef = useRef<HTMLDivElement>(null)
+//   const {mobile} = useContext(PreferencesContext)
+//   const {gameId, worldId, levelId} = useContext(GameIdContext)
+//   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
+//   const {proof, setProof} = useContext(ProofContext)
+//   const {deletedChat, setDeletedChat, showHelp, setShowHelp} = useContext(DeletedChatContext)
+//   const {selectedStep, setSelectedStep} = useContext(SelectionContext)
+//   const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
+
+//   let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
+
+//   function toggleSelection(line: number) {
+//     return (ev) => {
+//       console.debug('toggled selection')
+//       if (selectedStep == line) {
+//         setSelectedStep(undefined)
+//       } else {
+//         setSelectedStep(line)
+//       }
+//     }
+//   }
+
+//   useEffect(() => {
+//     // TODO: For some reason this is always called twice
+//     console.debug('scroll chat')
+//     if (!mobile) {
+//       chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0)
+//     }
+//   }, [proof, showHelp])
+
+//   // Scroll to element if selection changes
+//   useEffect(() => {
+//     if (typeof selectedStep !== 'undefined') {
+//       Array.from(chatRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => {
+//         elem.scrollIntoView({block: "center"})
+//       })
+//     }
+//   }, [selectedStep])
+
+//   // useEffect(() => {
+//   //   // // Scroll to top when loading a new level
+//   //   // // TODO: Thats the wrong behaviour probably
+//   //   // chatRef.current!.scrollTo(0,0)
+//   // }, [gameId, worldId, levelId])
+
+//   let introText: Array<string> = t(level?.data?.introduction, {ns: gameId}).split(/\n(\s*\n)+/)
+
+//   return <div className={`chat-panel ${visible ? '' : 'hidden'}`}>
+//     <div ref={chatRef} className="chat">
+//       {introText?.filter(t => t.trim()).map(((t, i) =>
+//         // Show the level's intro text as hints, too
+//         <Hint key={`intro-p-${i}`}
+//           hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
+//       ))}
+//       {proof?.steps.map((step, i) => {
+//         let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
+//         if (step.goals.length > 0 && !isLastStepWithErrors(proof, i)) {
+//           return <Hints key={`hints-${i}`}
+//           hints={filteredHints} showHidden={showHelp.has(i)} step={i}
+//           selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
+//         }
+//       })}
+
+//       {/* {modifiedHints.map((step, i) => {
+//         // It the last step has errors, it will have the same hints
+//         // as the second-to-last step. Therefore we should not display them.
+//         if (!(i == proof?.steps.length - 1 && withErr)) {
+//           // TODO: Should not use index as key.
+//           return <Hints key={`hints-${i}`}
+//             hints={step} showHidden={showHelp.has(i)} step={i}
+//             selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
+//         }
+//       })} */}
+//       <DeletedHints hints={deletedChat}/>
+//       {proof?.completed &&
+//         <>
+//           <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
+//             {t("Level completed! 🎉")}
+//           </div>
+//           {level?.data?.conclusion?.trim() &&
+//             <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
+//               <Markdown>{t(level?.data?.conclusion, {ns: gameId})}</Markdown>
+//             </div>
+//           }
+//         </>
+//       }
+//     </div>
+//     <div className="button-row">
+//       {proof?.completed && (lastLevel ?
+//         <Button to={`/${gameId}`}>
+//           <FontAwesomeIcon icon={faHome} />&nbsp;{t("Leave World")}
+//         </Button> :
+//         <Button to={`/${gameId}/world/${worldId}/level/${levelId + 1}`}>
+//           {t("Next")}&nbsp;<FontAwesomeIcon icon={faArrowRight} />
+//         </Button>)
+//         }
+//       <MoreHelpButton />
+//     </div>
+//   </div>
+// }
+
+
+export function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject<HTMLDivElement>, visible?: boolean}) {
+  const {gameId, worldId, levelId} = React.useContext(GameIdContext)
+  const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
+  const gameInfo = useGetGameInfoQuery({game: gameId})
+  return <div className={`exercise-panel ${visible ? '' : 'hidden'}`}>
+    <div className="">
+      <DualEditor level={level?.data} codeviewRef={codeviewRef} levelId={levelId} worldId={worldId} worldSize={gameInfo.data?.worldSize[worldId]}/>
+    </div>
+  </div>
+}
+
+
   // <Split minSize={0} snapOffset={200} sizes={[25, 75]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
   // <ChatPanel lastLevel={lastLevel}/>
   // <InventoryPanel />
   // </Split>
 
-function IntroductionPanel({gameInfo}) {
-  let { t } = useTranslation()
-  const {gameId} = React.useContext(GameIdContext)
-  const {worldId} = useContext(WorldLevelIdContext)
-  const {mobile} = React.useContext(PreferencesContext)
+// function IntroductionPanel({gameInfo}) {
+//   let { t } = useTranslation()
+//   const {gameId, worldId} = React.useContext(GameIdContext)
+//   const {mobile} = React.useContext(PreferencesContext)
 
-  let text: Array<string> = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).split(/\n(\s*\n)+/)
+//   let text: Array<string> = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).split(/\n(\s*\n)+/)
 
-  return <div className="chat-panel">
-    <div className="chat">
-      {text?.filter(t => t.trim()).map(((t, i) =>
-        <Hint key={`intro-p-${i}`}
-          hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={null} toggleSelection={undefined} />
-      ))}
-    </div>
-    <ChatButtons />
-  </div>
-}
+//   return <div className="chat-panel">
+//     <div className="chat">
+//       {text?.filter(t => t.trim()).map(((t, i) =>
+//         <Hint key={`intro-p-${i}`}
+//           hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={null} toggleSelection={undefined} />
+//       ))}
+//     </div>
+//     <ChatButtons />
+//   </div>
+// }
 
-export default Level
+// /** The site with the introduction text of a world */
+// function Introduction() {
+//   let { t } = useTranslation()
 
-/** The site with the introduction text of a world */
-function Introduction() {
-  let { t } = useTranslation()
+//   const {gameId, worldId} = React.useContext(GameIdContext)
+//   const {mobile} = useContext(PreferencesContext)
 
-  const {gameId} = React.useContext(GameIdContext)
-  const {mobile} = useContext(PreferencesContext)
+//   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
-  const inventory = useLoadInventoryOverviewQuery({game: gameId})
-
-  const gameInfo = useGetGameInfoQuery({game: gameId})
-
-  const {worldId} = useContext(WorldLevelIdContext)
-
-  let image: string = gameInfo.data?.worlds.nodes[worldId].image
+//   const gameInfo = useGetGameInfoQuery({game: gameId})
 
 
-  // const toggleImpressum = () => {
-  //   setImpressum(!impressum)
-  // }
-  // const togglePrivacy = () => {
-  //   setPrivacy(!privacy)
-  // }
-  return <>
-    {/* <LevelAppBar isLoading={gameInfo.isLoading} levelTitle={t("Introduction")} toggleImpressum={toggleImpressum} togglePrivacy={togglePrivacy} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/> */}
-    {gameInfo.isLoading ?
-      <div className="app-content loading"><CircularProgress /></div>
-    : mobile ?
-        <IntroductionPanel gameInfo={gameInfo} />
-      :
-        // <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level`}>
-        //   <IntroductionPanel gameInfo={gameInfo} />
-          <div className="world-image-container empty center">
-            {image &&
-              <img className="contain" src={path.join("data", gameId, image)} alt="" />
-            }
+//   let image: string = gameInfo.data?.worlds.nodes[worldId].image
 
-          </div>
-          // {/* <InventoryPanel /> */}
-        // </Split>
-      }
 
-  </>
-}
+//   // const toggleImpressum = () => {
+//   //   setImpressum(!impressum)
+//   // }
+//   // const togglePrivacy = () => {
+//   //   setPrivacy(!privacy)
+//   // }
+//   return <>
+//     {/* <LevelAppBar isLoading={gameInfo.isLoading} levelTitle={t("Introduction")} toggleImpressum={toggleImpressum} togglePrivacy={togglePrivacy} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/> */}
+//     {gameInfo.isLoading ?
+//       <div className="app-content loading"><CircularProgress /></div>
+//     : mobile ?
+//         <IntroductionPanel gameInfo={gameInfo} />
+//       :
+//         // <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level`}>
+//         //   <IntroductionPanel gameInfo={gameInfo} />
+//           <div className="world-image-container empty center">
+//             {image &&
+//               <img className="contain" src={path.join("data", gameId, image)} alt="" />
+//             }
+
+//           </div>
+//           // {/* <InventoryPanel /> */}
+//         // </Split>
+//       }
+
+//   </>
+// }
 
 // {mobile?
 //   // TODO: This is copied from the `Split` component below...
@@ -530,8 +617,7 @@ function Introduction() {
 
 function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) {
 
-  const {gameId} = React.useContext(GameIdContext)
-  const {worldId, levelId} = useContext(WorldLevelIdContext)
+  const {gameId, worldId, levelId} = React.useContext(GameIdContext)
 
   const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
   const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
@@ -544,6 +630,9 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
   const difficulty: number = useSelector(selectDifficulty(gameId))
 
   useEffect(() => {
+    // monaco.editor.getModels().forEach(model => model.dispose());
+
+    console.info(`trying to create model: ${gameId} ${worldId} ${levelId} ${uri}`)
     const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri)
     if (onDidChangeContent) {
       model.onDidChangeContent(() => onDidChangeContent(model.getValue()))

client/src/components/navigation.tsx

@@ -12,7 +12,7 @@ import { useTranslation } from 'react-i18next'
 import '../css/navigation.css'
 import { PopupContext } from './popup/popup'
 import { useSelector } from 'react-redux'
-import { selectCompleted, selectDifficulty, selectProgress } from '../state/progress'
+import { selectCompleted, selectDifficulty, selectProgress, selectReadIntro } from '../state/progress'
 import lean4gameConfig from '../config.json'
 import { Flag } from './flag'
 import { useAppSelector } from '../hooks'
@@ -34,8 +34,9 @@ export const NavButton: React.FC<{
   href?: string
   inverted?: boolean
   disabled?: boolean
-}> = ({icon, iconElement, text, onClick=()=>{}, title, href=null, inverted=false, disabled=false}) => {
-  return <a className={`nav-button btn${inverted?' btn-inverted':''}${disabled?' btn-disabled':''}`} onClick={disabled?null:onClick} href={disabled?null:href} title={title}>
+  className?: string
+}> = ({icon, iconElement, text, onClick=()=>{}, title, href=null, inverted=false, disabled=false, className=''}) => {
+  return <a className={`${className} nav-button btn${inverted?' btn-inverted':''}${disabled?' btn-disabled':''}`} onClick={disabled?null:onClick} href={disabled?null:href} title={title}>
     {iconElement ?? (icon && <FontAwesomeIcon icon={icon} />)}{text && <>&nbsp;{text}</>}
   </a>
 }
@@ -82,6 +83,9 @@ function MobileNavigationOverview () {
   const {page, setPage} = useContext(PageContext)
   const { setPopupContent } = useContext(PopupContext)
 
+  const { gameId, worldId } = useContext(GameIdContext)
+  const readIntro = useSelector(selectReadIntro(gameId, worldId))
+
   return <div className="nav-content">
     <div className="nav-title-left">
       <NavButton
@@ -106,6 +110,7 @@ function MobileNavigationOverview () {
           text={(page==0) ? t("Start") : null}
           icon={(page==0) ? null : faBook}
           onClick={() => setPage(page+1)}
+          disabled={!readIntro}
           inverted={true} />
       }
     </div>
@@ -123,13 +128,7 @@ function DesktopNavigationLevel () {
   const difficulty = useSelector(selectDifficulty(gameId))
   const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
 
-  /** toggle input mode if allowed */
-  function toggleInputMode(ev: React.MouseEvent) {
-    if (!lockEditorMode) {
-      setTypewriterMode(!typewriterMode)
-      console.log('test')
-    }
-  }
+  const readIntro = useSelector(selectReadIntro(gameId, worldId))
 
   const worldTitle = gameInfo.data?.worlds.nodes[worldId]?.title
   const levelTitle = ((levelId == 0) ?
@@ -166,22 +165,14 @@ function DesktopNavigationLevel () {
           icon={faHome}
           text={t("Leave World")}
           inverted={true}
-          disabled={difficulty == 0 || !completed}
+          disabled={levelId > 0 && difficulty == 2 && !completed}
           href={`#/${gameId}`} /> :
         <NavButton
           icon={faArrowRight}
           text={levelId == 0 ? t("Start") : t("Next")} inverted={true}
-          disabled={difficulty == 0 || !completed}
+          disabled={levelId == 0 ? !readIntro : (difficulty == 2 && !completed)}
           href={`#/${gameId}/world/${worldId}/level/${levelId + 1}`} />
       }
-      { levelId > 0 &&
-        <NavButton
-          icon={(typewriterMode && !lockEditorMode) ? faCode : faTerminal}
-          inverted={true}
-          disabled={levelId == 0 || lockEditorMode}
-          onClick={(ev) => toggleInputMode(ev)}
-          title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")} />
-      }
     </div>
   </div>
 }
@@ -228,6 +219,8 @@ export function Navigation () {
   const difficulty = useSelector(selectDifficulty(gameId))
   const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
 
+  const readIntro = useSelector(selectReadIntro(gameId, worldId))
+
   const [navOpen, setNavOpen] = useState(false)
   const [langNavOpen, setLangNavOpen] = useState(false)
   function toggleNav () {setNavOpen(!navOpen); setLangNavOpen(false)}
@@ -280,6 +273,7 @@ export function Navigation () {
             // Show all languages the game is available in
             gameInfo.data?.tile?.languages.map(iso =>
               <NavButton
+                key={`lang-selection-${iso}`}
                 iconElement={<Flag iso={iso} />}
                 text={lean4gameConfig.newLanguages[iso]?.name}
                 onClick={() => {setLanguage(iso)}}
@@ -287,6 +281,7 @@ export function Navigation () {
             // Show all languages the interface is available in (e.g. landing page)
             Object.entries(lean4gameConfig.newLanguages).map(([iso, val]) =>
               <NavButton
+                key={`lang-selection-${iso}`}
                 iconElement={<Flag iso={iso} />}
                 text={lean4gameConfig.newLanguages[iso]?.name}
                 onClick={() => {setLanguage(iso)}}
@@ -302,12 +297,12 @@ export function Navigation () {
                 icon={faHome}
                 text={t("Leave World")}
                 inverted={true}
-                disabled={difficulty == 0 || !completed}
+                disabled={levelId > 0 && difficulty == 2 && !completed}
                 href={`#/${gameId}`} /> :
               <NavButton
                 icon={faArrowRight}
                 text={levelId == 0 ? t("Start") : t("Next")} inverted={true}
-                disabled={difficulty == 0 || !completed}
+                disabled={levelId == 0 ? !readIntro : (difficulty == 2 && !completed)}
                 href={`#/${gameId}/world/${worldId}/level/${levelId + 1}`} />
             )}
             {mobile && levelId > 0 &&

client/src/components/popup/popup.tsx

@@ -48,9 +48,9 @@ export function Popup () {
   return <div className="modal-wrapper">
   <div className="modal-backdrop" onClick={closePopup} />
   <div className="modal">
-    <NavButton icon={faXmark}
+    {/* <NavButton icon={faXmark}
       onClick={closePopup}
-      inverted={true} />
+      inverted={true} /> */}
     <div className="codicon codicon-close modal-close" onClick={closePopup}></div>
     {Popups[popupContent]}
   </div>

client/src/components/typewriter.tsx

@@ -0,0 +1,7 @@
+import * as React from 'react'
+
+export function Typewriter () {
+  return <p>
+    I'm a typewriter
+  </p>
+}

client/src/components/welcome.tsx

@@ -7,7 +7,7 @@ import { faArrowRight } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
 import { useAppDispatch, useAppSelector } from '../hooks'
-import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
+import { changedReadIntro, selectReadIntro } from '../state/progress'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
 import { Button } from './button'
 import { PageContext, PreferencesContext } from './infoview/context'
@@ -55,7 +55,7 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string,
         <Button className="btn" to=""
           title="" onClick={() => {
             setPageNumber(1);
-            dispatch(changedOpenedIntro({game: gameId, openedIntro: true}))
+            dispatch(changedReadIntro({game: gameId, readIntro: true}))
           }}>
           Start&nbsp;<FontAwesomeIcon icon={faArrowRight}/>
         </Button>
@@ -66,7 +66,7 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string,
 
 /** main page of the game showing among others the tree of worlds/levels */
 function Welcome() {
-  const {gameId} = React.useContext(GameIdContext)
+  const {gameId, worldId} = React.useContext(GameIdContext)
 
   // Load the namespace of the game
   i18next.loadNamespaces(gameId)
@@ -78,13 +78,13 @@ function Welcome() {
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
   // For mobile only
-  const openedIntro = useAppSelector(selectOpenedIntro(gameId))
+  const readIntro = useAppSelector(selectReadIntro(gameId, worldId))
 
   const {page, setPage} = React.useContext(PageContext)
 
-  // TODO: recover `openedIntro` functionality
+  // TODO: recover `readIntro` functionality
 
-  // const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0)
+  // const [pageNumber, setPageNumber] = React.useState(readIntro ? 1 : 0)
 
   // pop-ups
   const [eraseMenu, setEraseMenu] = React.useState(false)

client/src/components/world_tree.tsx

@@ -197,47 +197,6 @@ export const downloadFile = ({ data, fileName, fileType } :
   a.remove()
 }
 
-/** The menu that is shown next to the world selection graph */
-export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
-  const { t, i18n } = useTranslation()
-  const {gameId} = React.useContext(GameIdContext)
-  const difficulty = useSelector(selectDifficulty(gameId))
-  const dispatch = useAppDispatch()
-  const { mobile } = React.useContext(PreferencesContext)
-
-
-  function label(x : number) {
-    return x == 0 ? t("none") : x == 1 ? t("relaxed") : t("regular")
-  }
-
-
-  return <nav className={`world-selection-menu${mobile ? '' : ' desktop'}`}>
-    <div className="slider-wrap">
-      <span className="difficulty-label">{t("Rules")}
-        <FontAwesomeIcon icon={rulesHelp ? faXmark : faCircleQuestion} className='helpButton' onClick={() => (setRulesHelp(!rulesHelp))}/>
-      </span>
-      <Slider
-        orientation="vertical"
-        title={t("Game Rules")}
-        min={0} max={2}
-        aria-label={t("Game Rules")}
-        value={difficulty}
-        marks={[
-          {value: 0, label: label(0)},
-          {value: 1, label: label(1)},
-          {value: 2, label: label(2)}
-        ]}
-        valueLabelFormat={label}
-        getAriaValueText={label}
-        valueLabelDisplay="off"
-        onChange={(ev, val: number) => {
-          dispatch(changedDifficulty({game: gameId, difficulty: val}))
-        }}
-        ></Slider>
-    </div>
-  </nav>
-}
-
 export function computeWorldLayout(worlds) {
   let elements = []
   for (let id in worlds.nodes) {
@@ -360,7 +319,7 @@ export function WorldTreePanel ({visible = true}) {
 
   let dx = bounds ? s*(bounds.x2 - bounds.x1) + 2*padding : null
 
-  return <div className={`column${visible ? '' : ' hidden'}`}>
+  return <div className={`${visible ? '' : 'hidden'}`}>
       {/* <WorldSelectionMenu rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} /> */}
       { gameInfo.data ?
       <svg xmlns="http://www.w3.org/2000/svg" xmlnsXlink="http://www.w3.org/1999/xlink"

client/src/config.json

@@ -37,5 +37,5 @@
       "name": "中文"
     }
   },
-  "useFlags": true
+  "useFlags": false
 }

client/src/css/chat.css

@@ -18,7 +18,24 @@
 }
 
 .message.deleted-hint {
-  background-color: #eee;
+  background-color: #EEE;
   color: #777;
-  box-shadow: .0em .0em .5em .2em #eee;
+  box-shadow: .0em .0em .5em .2em #EEE;
  }
+
+.message.success {
+  color: #000;
+  background-color: #E5FFDD;
+}
+
+
+.button-row > *:not(:last-child) {
+  /* display: block; */
+  margin-right: .2rem;
+}
+
+.button-row .btn-placeholder {
+  display: inline-block;
+  flex: 1;
+  margin: 0;
+}

client/src/css/game.css

@@ -23,6 +23,11 @@
 
 .column {
   width: 100%;
+  height: 100%;
+  overflow: auto;
+  position: relative;
+  scroll-behavior: smooth;
+
 }
 
 .slider .column {

client/src/css/infoview.css

@@ -70,13 +70,6 @@
   flex-direction: column;
 }
 
-.typewriter-interface .proof .MuiCircularProgress-root {
-  left: 50%;
-  position: relative;
-  margin-left: -20px;
-  margin-bottom: 0.6em;
-}
-
 .typewriter .typewriter-input {
   flex: 1;
 }
@@ -143,22 +136,12 @@
 }
 
 
-/* Push the goals to the bottom for now, until we insert the proof history above. */
-.typewriter-interface .content {
-  display: flex;
-  flex-direction: column;
-  scroll-behavior: smooth;
-}
 
 /* TODO this is in the wrong file */
 .chat {
   scroll-behavior: smooth;
 }
 
-.typewriter-interface .content .tmp-pusher {
-  flex: 1;
-}
-
 .exercise .command {
   background-color: #bbb;
   padding: .5em;

client/src/css/inventory.css

@@ -46,9 +46,14 @@
   background-color: rgb(255, 242, 190);
 }
 
+.inventory .item.current-world {
+  background-color: rgb(250, 231, 255);
+}
+
 .inventory .item.recent {
   background-color: rgb(242, 190, 255);
 }
+
 .inventory .item:not(.locked), .inventory .item.enabled {
   cursor: pointer;
 }

client/src/css/level.css

@@ -5,12 +5,12 @@
   /* display: flex; */
 }
 
-.inventory-panel, .exercise-panel, .doc-panel, .introduction-panel {
+/* .inventory-panel, .exercise-panel, .doc-panel, .introduction-panel {
   height: 100%;
   width: 100%;
   overflow: auto;
   position: relative;
-}
+} */
 
 .infoview {
   padding-top: 1em;
@@ -44,11 +44,11 @@
   padding-top: 0em;
 }
 
-.exercise {
+/* .exercise {
   flex: 1 1 auto;
   display: flex;
   flex-flow: column;
-}
+} */
 
 .codeview {
   flex: 1 1 auto;
@@ -216,12 +216,6 @@ td code  {
   padding: .5em;
 }
 
-/* .exercise-panel {
-  display: flex;
-  flex-flow: column;
-  height: 100%;
-} */
-
 /* .button-row.mobile {
   margin: .5rem;
   padding-top: .2rem;
@@ -236,17 +230,18 @@ td code  {
 } */
 
 
-.typewriter-interface {
+.exercise-content {
   display: flex;
   flex-flow: column;
   height: 100%;
+  z-index: 1;
 }
 
 .typewriter {
   flex: 0 1 auto;
 }
 
-.typewriter-interface .content {
+.exercise-content {
   flex: 1 1 auto;
   overflow-y: scroll;
   padding: 0;
@@ -332,22 +327,31 @@ td code  {
   justify-content: center;
 }
 
-.typewriter-interface .content, .world-image-container.empty {
+.exercise {
   background-color: #eee;
+  position: relative;
 }
 
-.world-image-container {
+.world-image {
+  height: 100%;
+  width: 100%;
+  overflow: hidden;
   display: flex;
   flex-direction: column;
-  min-height: 0px; /* somehow this has a desired affect, but why? */
-  overflow: hidden;
+  position: absolute;
+  z-index: 0;
+  /* min-height: 0px;*/ /* somehow this has a desired affect, but why? */
 }
 
-.world-image-container img.contain {
+.world-image img.contain {
+  height: 100%;
+  width: 100%;
   object-fit: contain;
+  object-position: top center;
+  pointer-events: none;
 }
 
-.world-image-container.center {
+.world-image.center {
   justify-content: center;
 }
 
@@ -357,10 +361,33 @@ td code  {
   object-fit: cover;
 }
 
-.typewriter-interface .proof {
+.proof {
+  z-index: 2;
   background-color: #fff;
 }
 
+.exercise-content .tmp-pusher {
+  flex: 1;
+}
+
+.exercise-content {
+  background: none;
+}
+
+/* Push the goals to the bottom for now, until we insert the proof history above. */
+.exercise-content {
+  display: flex;
+  flex-direction: column;
+  scroll-behavior: smooth;
+}
+
+.exercise-content .proof .MuiCircularProgress-root {
+  left: 50%;
+  position: relative;
+  margin-left: -20px;
+  margin-bottom: 0.6em;
+}
+
 .toggle-width {
   min-width: 40px;
   text-align: center;

client/src/css/navigation.css

@@ -75,3 +75,23 @@ nav {
 .dropdown .svg-inline--fa {
   width: 1.8rem;
 }
+
+.btn-right {
+  float: right;
+  margin: 0.2rem;
+}
+
+.btn-input-mode {
+  position: absolute;
+  right: 0.4rem;
+  z-index: 5;
+  top: 0.4rem;
+  margin: 0;
+  border: 1px solid var(--clr-primary);
+  background-color: #eee;
+  font-size: .7rem;
+  /* box-shadow: .0em .0em .4em .1em var(--clr-primary); */
+  /* box-shadow: -.1rem .3rem .3rem 0 var(--clr-primary); */
+  /* border-top-right-radius: 0;
+  border-bottom-right-radius: 0; */
+}

client/src/index.tsx

@@ -8,7 +8,6 @@ import { createHashRouter, RouterProvider, Route, redirect } from "react-router-
 import ErrorPage from './components/error_page'
 import Welcome from './components/welcome'
 import LandingPage from './components/landing_page'
-import Level from './components/level'
 import './i18n';
 import Game from './components/game'
 

client/src/state/api.ts

@@ -85,7 +85,7 @@ export const apiSlice = createApi({
     }),
     loadLevel: builder.query<LevelInfo, {game: string, world: string, level: number}>({
       query: ({game, world, level}) => {
-        if (world) {
+        if (world && level > 0) {
           return `${game}/level__${world}__${level}.json`
         } else {
           return `${game}/inventory.json`

client/src/state/progress.ts

@@ -19,13 +19,13 @@ interface LevelProgressState {
   help: number[], // A set of rows where hidden hints have been displayed
 }
 interface WorldProgressState {
-  [world: string] : {[level: number]: LevelProgressState},
+  [world: string] : {[level: number]: LevelProgressState, readIntro: boolean},
 }
 
 export interface GameProgressState {
   inventory: string[],
   difficulty: number,
-  openedIntro: boolean,
+  readIntro: boolean,
   data: WorldProgressState,
   typewriterMode?: boolean
 }
@@ -54,19 +54,24 @@ const initalLevelProgressState: LevelProgressState = {code: "", completed: false
 /** Add an empty skeleton with progress for the current game */
 function addGameProgress (state: ProgressState, action: PayloadAction<{game: string}>) {
   if (!state.games[action.payload.game.toLowerCase()]) {
-    state.games[action.payload.game.toLowerCase()] = {inventory: [], openedIntro: false, data: {}, difficulty: DEFAULT_DIFFICULTY}
+    state.games[action.payload.game.toLowerCase()] = {inventory: [], readIntro: false, data: {}, difficulty: DEFAULT_DIFFICULTY}
   }
   if (!state.games[action.payload.game.toLowerCase()].data) {
     state.games[action.payload.game.toLowerCase()].data = {}
   }
 }
 
+function addWorldProgress(state: ProgressState, action: PayloadAction<{game: string, world: string}>) {
+  addGameProgress(state, action)
+  if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world]) {
+    state.games[action.payload.game.toLowerCase()].data[action.payload.world] = {readIntro: false}
+  }
+}
+
 /** Add an empty skeleton with progress for the current level */
 function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
   addGameProgress(state, action)
-  if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world]) {
-    state.games[action.payload.game.toLowerCase()].data[action.payload.world] = {}
-  }
+  addWorldProgress(state, action)
   if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level]) {
     state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level] = {...initalLevelProgressState}
   }
@@ -80,7 +85,7 @@ export const progressSlice = createSlice({
     codeEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, code: string}>) {
       addLevelProgress(state, action)
       state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].code = action.payload.code
-      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = false
+      // state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = false
     },
     /** TODO: docstring */
     changedSelection(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, selections: Selection[]}>) {
@@ -100,7 +105,7 @@ export const progressSlice = createSlice({
     },
     /** delete all progress for this game */
     deleteProgress(state: ProgressState, action: PayloadAction<{game: string}>) {
-      state.games[action.payload.game.toLowerCase()] = {inventory: [], data: {}, openedIntro: false, difficulty: DEFAULT_DIFFICULTY}
+      state.games[action.payload.game.toLowerCase()] = {inventory: [], data: {}, readIntro: false, difficulty: DEFAULT_DIFFICULTY}
     },
     /** delete progress for this level */
     deleteLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
@@ -123,9 +128,13 @@ export const progressSlice = createSlice({
       state.games[action.payload.game.toLowerCase()].difficulty = action.payload.difficulty
     },
     /** set the difficulty */
-    changedOpenedIntro(state: ProgressState, action: PayloadAction<{game: string, openedIntro: boolean}>) {
-      addGameProgress(state, action)
-      state.games[action.payload.game.toLowerCase()].openedIntro = action.payload.openedIntro
+    changedReadIntro(state: ProgressState, action: PayloadAction<{game: string, world: string, readIntro: boolean}>) {
+      addWorldProgress(state, action)
+      if (action.payload.world) {
+        state.games[action.payload.game.toLowerCase()].data[action.payload.world].readIntro = action.payload.readIntro
+      } else {
+        state.games[action.payload.game.toLowerCase()].readIntro = action.payload.readIntro
+      }
     },
     /** set the typewriter mode */
     changeTypewriterMode(state: ProgressState, action: PayloadAction<{game: string, typewriterMode: boolean}>) {
@@ -137,47 +146,47 @@ export const progressSlice = createSlice({
 
 /** if the level does not exist, return default values */
 export function selectLevel(game: string, world: string, level: number) {
-  return (state) =>{
-    if (!state.progress.games[game.toLowerCase()]) { return initalLevelProgressState }
-    if (!state.progress.games[game.toLowerCase()].data[world]) { return initalLevelProgressState }
-    if (!state.progress.games[game.toLowerCase()].data[world][level]) { return initalLevelProgressState }
-    return state.progress.games[game.toLowerCase()].data[world][level]
+  return (state) => {
+    if (!state.progress.games[game?.toLowerCase()]) { return initalLevelProgressState }
+    if (!state.progress.games[game?.toLowerCase()].data[world]) { return initalLevelProgressState }
+    if (!state.progress.games[game?.toLowerCase()].data[world][level]) { return initalLevelProgressState }
+    return state.progress.games[game?.toLowerCase()].data[world][level]
   }
 }
 
 /** return the code of the current level */
 export function selectCode(game: string, world: string, level: number) {
   return (state) => {
-    return selectLevel(game.toLowerCase(), world, level)(state).code
+    return selectLevel(game?.toLowerCase(), world, level)(state).code
   }
 }
 
 /** return the current inventory */
 export function selectInventory(game: string) {
   return (state) => {
-    if (!state.progress.games[game.toLowerCase()]) { return [] }
-    return state.progress.games[game.toLowerCase()].inventory
+    if (!state.progress.games[game?.toLowerCase()]) { return [] }
+    return state.progress.games[game?.toLowerCase()].inventory
   }
 }
 
 /** return the code of the current level */
 export function selectHelp(game: string, world: string, level: number) {
   return (state) => {
-    return selectLevel(game.toLowerCase(), world, level)(state).help
+    return selectLevel(game?.toLowerCase(), world, level)(state).help
   }
 }
 
 /** return the selections made in the current level */
 export function selectSelections(game: string, world: string, level: number) {
   return (state) => {
-    return selectLevel(game.toLowerCase(), world, level)(state).selections
+    return selectLevel(game?.toLowerCase(), world, level)(state).selections
   }
 }
 
 /** return whether the current level is clompleted */
 export function selectCompleted(game: string, world: string, level: number) {
   return (state) => {
-    return selectLevel(game.toLowerCase(), world, level)(state).completed
+    return selectLevel(game?.toLowerCase(), world, level)(state).completed
   }
 }
 
@@ -191,14 +200,17 @@ export function selectProgress(game: string) {
 /** return difficulty for the current game if it exists */
 export function selectDifficulty(game: string) {
   return (state) => {
-    return state.progress.games[game.toLowerCase()]?.difficulty ?? DEFAULT_DIFFICULTY
+    return state.progress.games[game?.toLowerCase()]?.difficulty ?? DEFAULT_DIFFICULTY
   }
 }
 
 /** return whether the intro has been read */
-export function selectOpenedIntro(game: string) {
+export function selectReadIntro(game: string, worldId: string) {
   return (state) => {
-    return state.progress.games[game?.toLowerCase()]?.openedIntro
+    if (worldId) {
+      return state.progress.games[game?.toLowerCase()].data[worldId]?.readIntro
+    }
+    return state.progress.games[game?.toLowerCase()]?.readIntro
   }
 }
 
@@ -211,5 +223,5 @@ export function selectTypewriterMode(game: string) {
 
 /** Export actions to modify the progress */
 export const { changedSelection, codeEdited, levelCompleted, deleteProgress,
-  deleteLevelProgress, loadProgress, helpEdited, changedInventory, changedOpenedIntro,
+  deleteLevelProgress, loadProgress, helpEdited, changedInventory, changedReadIntro,
   changedDifficulty, changeTypewriterMode} = progressSlice.actions