Merge branch 'dev' into world_overviews

WIP progress on world overviews
2023-12-10 00:18:47 +01:00 · 2023-10-23 15:41:29 +02:00
37 changed files with 1529 additions and 1150 deletions
@@ -9,37 +9,25 @@ import '@fontsource/roboto/700.css';
 import './css/reset.css';
 import './css/app.css';
 import { MobileContext } from './components/infoview/context';
-import { useMobile } from './hooks';
-import { AUTO_SWITCH_THRESHOLD, getWindowDimensions} from './state/preferences';
+import { useWindowDimensions } from './window_width';
+import { connection } from './connection';

 export const GameIdContext = React.createContext<string>(undefined);

 function App() {
-  const { mobile, setMobile, lockMobile, setLockMobile } = useMobile();
-
  const params = useParams()
  const gameId = "g/" + params.owner + "/" + params.repo
+  const {width, height} = useWindowDimensions()
+  const [mobile, setMobile] = React.useState(width < 800)

-  const automaticallyAdjustLayout = () => {
-    const {width} = getWindowDimensions()
-    setMobile(width < AUTO_SWITCH_THRESHOLD)
-  }
-
-  React.useEffect(()=>{
-    if (!lockMobile){
-      void automaticallyAdjustLayout()
-      window.addEventListener('resize', automaticallyAdjustLayout)
-
-      return () => {
-        window.removeEventListener('resize', automaticallyAdjustLayout)
-      }
-    }
-  }, [lockMobile])
+  React.useEffect(() => {
+    connection.startLeanClient(gameId);
+  }, [gameId])

  return (
    <div className="app">
      <GameIdContext.Provider value={gameId}>
-        <MobileContext.Provider value={{mobile, setMobile, lockMobile, setLockMobile}}>
+        <MobileContext.Provider value={{mobile, setMobile}}>
          <Outlet />
        </MobileContext.Provider>
      </GameIdContext.Provider>
@@ -5,7 +5,7 @@ import * as React from 'react'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
  faArrowRight, faArrowLeft, faXmark, faBars, faCode,
-  faCircleInfo, faTerminal, faMobileScreenButton, faDesktop, faGear } from '@fortawesome/free-solid-svg-icons'
+  faCircleInfo, faTerminal } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from "../app"
 import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context"
 import { GameInfo, useGetGameInfoQuery } from '../state/api'
@@ -150,23 +150,22 @@ function InventoryButton({pageNumber, setPageNumber}) {
 }

 /** the navigation bar on the welcome page */
-export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo, togglePreferencesPopup} : {
+export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo} : {
  pageNumber: number,
  setPageNumber: any,
  gameInfo: GameInfo,
  toggleImpressum: any,
  toggleEraseMenu: any,
  toggleUploadMenu: any,
-  toggleInfo: any,
-  togglePreferencesPopup: () => void;
+  toggleInfo: any
 }) {
  const gameId = React.useContext(GameIdContext)
  const gameProgress = useAppSelector(selectProgress(gameId))
-  const {mobile, setMobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(MobileContext)
  const [navOpen, setNavOpen] = React.useState(false)

  return <div className="app-bar">
-    <div className='app-bar-left'>
+    <div>
      <Button inverted="false" title="back to games selection" to="/">
        <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
      </Button>
@@ -195,9 +194,6 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres
      <Button title="Impressum, privacy policy" inverted="true" to="" onClick={() => {toggleImpressum(); setNavOpen(false)}}>
        <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Impressum
      </Button>
-      <Button title="Preferences" inverted="true" to="" onClick={() => {togglePreferencesPopup(); setNavOpen(false)}}>
-         <FontAwesomeIcon icon={faGear} />&nbsp;Preferences
-       </Button>
    </div>
  </div>
 }
@@ -241,7 +237,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=
      </> :
      <>
        {/* DESKTOP VERSION */}
-        <div className='app-bar-left'>
+        <div>
          <HomeButton isDropdown={false} />
          <span className="app-bar-title">{worldTitle && `World: ${worldTitle}`}</span>
        </div>
@@ -62,18 +62,12 @@ export const ProofStateContext = React.createContext<{
  setProofState: () => {},
 })

-export interface IMobileContext {
+export const MobileContext = React.createContext<{
  mobile : boolean,
  setMobile: React.Dispatch<React.SetStateAction<Boolean>>,
-  lockMobile: boolean,
-  setLockMobile: React.Dispatch<React.SetStateAction<Boolean>>,
-}
-
-export const MobileContext = React.createContext<IMobileContext>({
-  mobile: false,
+}>({
+  mobile : false,
  setMobile: () => {},
-  lockMobile: false,
-  setLockMobile: () => {}
 })

 export const WorldLevelIdContext = React.createContext<{
@@ -493,20 +493,18 @@ export function TypewriterInterface({props}) {
                      <Markdown>{props.data?.introduction}</Markdown>
                    </div>
                  }
-                  {mobile &&
+                  {mobile && <>
                    <Hints key={`hints-${i}`}
                      hints={step.hints} showHidden={showHelp.has(i)} step={i}
                      selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
+                    {i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
+                      <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
+                        Show more help!
+                      </Button>
+                    }
+                  </>
                  }
                  <GoalsTabs proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/>
-
-                  {mobile && i == proof.length - 1 &&
-                    hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
-                    <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
-                      Show more help!
-                    </Button>
-                  }
-
                  {/* Show a message that there are no goals left */}
                  {!step.goals.length && (
                    <div className="message information">
@@ -523,7 +521,7 @@ export function TypewriterInterface({props}) {
              }
            })}
            {mobile && completed &&
-              <div className="button-row mobile">
+              <div className="button-row">
                {props.level >= props.worldSize ?
                  <Button to={`/${gameId}`}>
                    <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
@@ -2,21 +2,18 @@ import * as React from 'react';
 import { useState, useEffect } from 'react';
 import '../css/inventory.css'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faLock, faBan, faCheck } from '@fortawesome/free-solid-svg-icons'
-import { faClipboard } from '@fortawesome/free-regular-svg-icons'
+import { faLock, faBan } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from '../app';
 import Markdown from './markdown';
-import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api';
+import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery, WorldOverview } from '../state/api';
 import { selectDifficulty, selectInventory } from '../state/progress';
 import { store } from '../state/store';
 import { useSelector } from 'react-redux';

-export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=false} :
+export function Inventory({levelInfo, openDoc, enableAll=false} :
  {
    levelInfo: LevelInfo|InventoryOverview,
    openDoc: (props: {name: string, type: string}) => void,
-    lemmaTab: any,
-    setLemmaTab: any,
    enableAll?: boolean,
  }) {

@@ -34,20 +31,92 @@ export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=
      }
      <h2>Theorems</h2>
      {levelInfo?.lemmas &&
-        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} level={levelInfo} enableAll={enableAll} tab={lemmaTab} setTab={setLemmaTab}/>
+        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} defaultTab={levelInfo?.lemmaTab} level={levelInfo} enableAll={enableAll}/>
      }
    </div>
  )
 }

-function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, level=undefined, enableAll=false} :
+export function OverviewInventory({data, openDoc, enableAll=false, showOverview=true} :
+  {
+    data: WorldOverview[],
+    openDoc: (props: {name: string, type: string}) => void,
+    enableAll?: boolean,
+    showOverview?: boolean
+  }) {
+
+  const gameId = React.useContext(GameIdContext)
+  const difficulty = useSelector(selectDifficulty(gameId))
+  const [tab, setTab] = useState<string>()
+  let inv: string[] = selectInventory(gameId)(store.getState())
+
+  let levelInfo : InventoryOverview = {
+    tactics : data ? data.map(world => (world.tactics.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile))).flat() : [],
+    lemmas : data ? data.map(world => (world.lemmas.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile))).flat() : [],
+    definitions : data ? data.map(world => (world.definitions.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile))).flat() : [],
+    lemmaTab: null,
+  }
+
+  return (
+    <>
+      <Inventory levelInfo={levelInfo} openDoc={openDoc} enableAll={enableAll}/>
+      {showOverview &&
+        <div className="inventory">
+          {data && <>
+            <h2>Overviews</h2>
+            <div className="tab-bar">
+              {data.map(world => {
+                return <div key={`category-${world.world}`} className={`tab ${world.world == tab ? "active": ""}`} onClick={() => { setTab((tab == world.world) ? null : world.world) }}>{world.world}</div>
+              })}
+            </div>
+            <div className="inventory-list">
+              {/* TODO: a bit hacky, do we need to redesign inventory completely and provide it in a better order? */}
+              {data.map(world => {
+                if (world.world == tab) {
+                  return [
+                    ...world.tactics.map(item => {
+                      return <InventoryItem
+                        key={`${world.world}-${item.name}`}
+                        showDoc={() => {openDoc({name: item.name, type: 'Tactic'})}}
+                        name={item.name} displayName={item.displayName}
+                        locked={difficulty > 0 ? !inv.includes(item.name) : false}
+                        disabled={item.disabled} newly={false} enableAll={enableAll} />
+                    }),
+                    ...world.lemmas.map(item => {
+                      return <InventoryItem
+                        key={`${world.world}-${item.name}`}
+                        showDoc={() => {openDoc({name: item.name, type: 'Lemma'})}}
+                        name={item.name} displayName={item.displayName}
+                        locked={difficulty > 0 ? item.locked : false}
+                        disabled={item.disabled} newly={false} enableAll={enableAll} />
+                    }),
+                    ...world.definitions.map(item => {
+                      return <InventoryItem
+                        key={`${world.world}-${item.name}`}
+                        showDoc={() => {openDoc({name: item.name, type: 'Definition'})}}
+                        name={item.name} displayName={item.displayName}
+                        locked={difficulty > 0 ? item.locked : false}
+                        disabled={item.disabled} newly={false} enableAll={enableAll} />
+                    })
+                  ]
+                }
+              })}
+            </div>
+          </>}
+        </div>
+      }
+    </>
+
+  )
+}
+
+function InventoryList({items, docType, openDoc, defaultTab=null, level=undefined, enableAll=false} :
  {
    items: InventoryTile[],
    docType: string,
    openDoc(props: {name: string, type: string}): void,
-    tab?: any,
-    setTab?: any,
-    level?: LevelInfo|InventoryOverview,
+    defaultTab? : string,
+    level? : LevelInfo|InventoryOverview,
    enableAll?: boolean,
  }) {
  // TODO: `level` is only used in the `useEffect` below to check if a new level has
@@ -63,6 +132,8 @@ function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, lev
  }
  const categories = Array.from(categorySet).sort()

+  const [tab, setTab] = useState(defaultTab)
+
  // Add inventory items from local store as unlocked.
  // Items are unlocked if they are in the local store, or if the server says they should be
  // given the dependency graph. (OR-connection) (TODO: maybe add different logic for different
@@ -70,6 +141,13 @@ function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, lev
  let inv: string[] = selectInventory(gameId)(store.getState())
  let modifiedItems : InventoryTile[] = items.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile)

+  useEffect(() => {
+    // If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading.
+    // `defaultTab` is `null` or `undefined` otherwise, in which case we don't want to switch.
+    if (defaultTab) {
+      setTab(defaultTab)
+    }}, [level])
+
  return <>
    {categories.length > 1 &&
      <div className="tab-bar">
@@ -84,26 +162,21 @@ function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, lev
          (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName)
        ).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => {
            return <InventoryItem key={`${item.category}-${item.name}`}
-              item={item}
              showDoc={() => {openDoc({name: item.name, type: docType})}}
              name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false}
-              disabled={item.disabled} newly={item.new} enableAll={enableAll} />
+              disabled={item.disabled} newly={item.new} enableAll={enableAll}/>
        })
      }
    </div>
    </>
 }

-function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, enableAll=false}) {
+function InventoryItem({name, displayName, locked, disabled, newly, showDoc, enableAll=false}) {
  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 ? "Not unlocked yet" :
-                disabled ? "Not available in this level" : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
-
-  const [copied, setCopied] = useState(false)
+                disabled ? "Not available in this level" : ""

  const handleClick = () => {
    if (enableAll || !locked) {
@@ -111,21 +184,7 @@ function InventoryItem({item, name, displayName, locked, disabled, newly, showDo
    }
  }

-  const copyItemName = (ev) => {
-    navigator.clipboard.writeText(displayName)
-    setCopied(true)
-    setInterval(() => {
-      setCopied(false)
-    }, 3000);
-    ev.stopPropagation()
-  }
-
-return <div className={`item ${className}${enableAll ? ' enabled' : ''}`} onClick={handleClick} title={title}>
-    {icon} {displayName}
-    <div className="copy-button" onClick={copyItemName}>
-      {copied ? <FontAwesomeIcon icon={faCheck} /> : <FontAwesomeIcon icon={faClipboard} />}
-    </div>
-  </div>
+  return <div className={`item ${className}${enableAll ? ' enabled' : ''}`} onClick={handleClick} title={title}>{icon} {displayName}</div>
 }

 export function Documentation({name, type, handleClose}) {
@@ -145,25 +204,34 @@ export function Documentation({name, type, handleClose}) {
 export function InventoryPanel({levelInfo, visible = true}) {
  const gameId = React.useContext(GameIdContext)

-  const [lemmaTab, setLemmaTab] = useState(levelInfo?.lemmaTab)
+  // The inventory is overlayed by the doc entry of a clicked item
+  const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
+  // Set `inventoryDoc` to `null` to close the doc
+  function closeInventoryDoc() {setInventoryDoc(null)}
+
+  return <div className={`column inventory-panel ${visible ? '' : 'hidden'}`}>
+    {inventoryDoc ?
+      <Documentation name={inventoryDoc.name} type={inventoryDoc.type} handleClose={closeInventoryDoc}/>
+      :
+      <Inventory levelInfo={levelInfo} openDoc={setInventoryDoc} enableAll={true}/>
+    }
+  </div>
+}
+
+/** The panel (on the welcome page) showing the user's inventory with tactics, definitions, and lemmas */
+export function InventoryOverviewPanel({data, visible = true, showOverview=true} : {data : WorldOverview[], visible?: boolean, showOverview?: boolean}) {
+  const gameId = React.useContext(GameIdContext)

  // The inventory is overlayed by the doc entry of a clicked item
  const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
  // Set `inventoryDoc` to `null` to close the doc
  function closeInventoryDoc() {setInventoryDoc(null)}

-    useEffect(() => {
-    // If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading.
-    // `defaultTab` is `null` or `undefined` otherwise, in which case we don't want to switch.
-    if (levelInfo?.lemmaTab) {
-      setLemmaTab(levelInfo?.lemmaTab)
-    }}, [levelInfo])
-
  return <div className={`column inventory-panel ${visible ? '' : 'hidden'}`}>
    {inventoryDoc ?
      <Documentation name={inventoryDoc.name} type={inventoryDoc.type} handleClose={closeInventoryDoc}/>
      :
-      <Inventory levelInfo={levelInfo} openDoc={setInventoryDoc} enableAll={true} lemmaTab={lemmaTab} setLemmaTab={setLemmaTab}/>
+      <OverviewInventory data={data} openDoc={setInventoryDoc} enableAll={true} showOverview={showOverview}/>
    }
  </div>
 }
@@ -18,6 +18,7 @@ import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-info
 import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event'

 import { GameIdContext } from '../app'
+import { ConnectionContext, connection, useLeanClient } from '../connection'
 import { useAppDispatch, useAppSelector } from '../hooks'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api'
 import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited,
@@ -25,7 +26,7 @@ import { changedSelection, codeEdited, selectCode, selectSelections, selectCompl
 import { store } from '../state/store'
 import { Button } from './button'
 import Markdown from './markdown'
-import {InventoryPanel} from './inventory'
+import {InventoryOverviewPanel, InventoryPanel} from './inventory'
 import { hasInteractiveErrors } from './infoview/typewriter'
 import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext,
  ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
@@ -43,15 +44,6 @@ import 'lean4web/client/src/editor/infoview.css'
 import 'lean4web/client/src/editor/vscode.css'
 import '../css/level.css'
 import { LevelAppBar } from './app_bar'
-import { LeanClient } from 'lean4web/client/src/editor/leanclient'
-import { DisposingWebSocketMessageReader } from 'lean4web/client/src/reader'
-import { WebSocketMessageWriter, toSocket } from 'vscode-ws-jsonrpc'
-import { IConnectionProvider } from 'monaco-languageclient'
-import { monacoSetup } from 'lean4web/client/src/monacoSetup'
-import { onigasmH } from 'onigasm/lib/onigasmH'
-
-
-monacoSetup()

 function Level() {
  const params = useParams()
@@ -219,8 +211,10 @@ function PlayableLevel({impressum, setImpressum}) {

  const dispatch = useAppDispatch()

+  const difficulty = useSelector(selectDifficulty(gameId))
  const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
  const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
+  const inventory: Array<String> = useSelector(selectInventory(gameId))

  const typewriterMode = useSelector(selectTypewriterMode(gameId))
  const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
@@ -299,6 +293,12 @@ function PlayableLevel({impressum, setImpressum}) {
  // a hint at the beginning of the proof...
  const [selectedStep, setSelectedStep] = useState<number>()

+  // if the user inventory changes, notify the server
+  useEffect(() => {
+    let leanClient = connection.getLeanClient(gameId)
+    leanClient.sendNotification('$/game/setInventory', {inventory: inventory, difficulty: difficulty})
+  }, [inventory])
+
  useEffect (() => {
    // Lock editor mode
    if (level?.data?.template) {
@@ -372,7 +372,7 @@ function PlayableLevel({impressum, setImpressum}) {

  // Effect when command line mode gets enabled
  useEffect(() => {
-    if (onigasmH && editor && typewriterMode) {
+    if (editor && typewriterMode) {
      let code = editor.getModel().getLinesContent().filter(line => line.trim())
      editor.executeEdits("typewriter", [{
        range: editor.getModel().getFullModelRange(),
@@ -395,7 +395,7 @@ function PlayableLevel({impressum, setImpressum}) {
      //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
      // }
    }
-  }, [editor, typewriterMode, onigasmH == null])
+  }, [editor, typewriterMode])

  return <>
    <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
@@ -441,7 +441,6 @@ function PlayableLevel({impressum, setImpressum}) {
 function IntroductionPanel({gameInfo}) {
  const gameId = React.useContext(GameIdContext)
  const {worldId} = useContext(WorldLevelIdContext)
-  const {mobile} = React.useContext(MobileContext)

  let text: Array<string> = gameInfo.data?.worlds.nodes[worldId].introduction.split(/\n(\s*\n)+/)

@@ -452,7 +451,7 @@ function IntroductionPanel({gameInfo}) {
          hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
      ))}
    </div>
-    <div className={`button-row${mobile ? ' mobile' : ''}`}>
+    <div className="button-row">
      {gameInfo.data?.worldSize[worldId] == 0 ?
        <Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
        <Button to={`/${gameId}/world/${worldId}/level/1`}>
@@ -499,7 +498,7 @@ function Introduction({impressum, setImpressum}) {
            }

          </div>
-          <InventoryPanel levelInfo={inventory?.data} />
+          <InventoryOverviewPanel data={inventory?.data} />
        </Split>
      }

@@ -531,32 +530,21 @@ function Introduction({impressum, setImpressum}) {

 function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) {

+  const connection = React.useContext(ConnectionContext)
  const gameId = React.useContext(GameIdContext)
  const {worldId, levelId} = useContext(WorldLevelIdContext)

+
  const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
  const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
+  const [infoviewApi, setInfoviewApi] = useState<null|InfoviewApi>(null)
  const [editorConnection, setEditorConnection] = useState<null|EditorConnection>(null)

-  const uriStr = `file:///${worldId}/${levelId}`
-  const uri = monaco.Uri.parse(uriStr)
-
-  const inventory: Array<String> = useSelector(selectInventory(gameId))
-  const difficulty: number = useSelector(selectDifficulty(gameId))
-
+  // Create Editor
  useEffect(() => {
-    const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri)
-    if (onDidChangeContent) {
-      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
-    }
-
    const editor = monaco.editor.create(codeviewRef.current!, {
-      model,
      glyphMargin: true,
      quickSuggestions: false,
-      lineDecorationsWidth: 5,
-      folding: false,
-      lineNumbers: 'on',
      lightbulb: {
        enabled: true
      },
@@ -568,61 +556,11 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
        enabled: false
      },
      lineNumbersMinChars: 3,
-      tabSize: 2,
      'semanticHighlighting.enabled': true,
      theme: 'vs-code-theme-converted'
    })
-    if (onDidChangeSelection) {
-      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
-    }
-    if (initialSelections) {
-      console.debug("Initial Selection: ", initialSelections)
-      // BUG: Somehow I get an `invalid arguments` bug here
-      // editor.setSelections(initialSelections)
-    }
-    setEditor(editor)
-    const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)

-    const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + gameId
-
-    const connectionProvider : IConnectionProvider = {
-      get: async () => {
-        return await new Promise((resolve, reject) => {
-          console.log(`connecting ${socketUrl}`)
-          const websocket = new WebSocket(socketUrl)
-          websocket.addEventListener('error', (ev) => {
-            reject(ev)
-          })
-          websocket.addEventListener('message', (msg) => {
-            // console.log(msg.data)
-          })
-          websocket.addEventListener('open', () => {
-            const socket = toSocket(websocket)
-            const reader = new DisposingWebSocketMessageReader(socket)
-            const writer = new WebSocketMessageWriter(socket)
-            resolve({
-              reader,
-              writer
-            })
-          })
-        })
-      }
-    }
-
-    // Following `vscode-lean4/webview/index.ts`
-    const client = new LeanClient(connectionProvider, showRestartMessage, {inventory, difficulty})
-    const infoProvider = new InfoProvider(client)
-    // const div: HTMLElement = infoviewRef.current!
-    const imports = {
-      '@leanprover/infoview': `${window.location.origin}/index.production.min.js`,
-      'react': `${window.location.origin}/react.production.min.js`,
-      'react/jsx-runtime': `${window.location.origin}/react-jsx-runtime.production.min.js`,
-      'react-dom': `${window.location.origin}/react-dom.production.min.js`,
-      'react-popper': `${window.location.origin}/react-popper.production.min.js`
-    }
-    // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi)
-    setInfoProvider(infoProvider)
-    client.restart()
+    const infoProvider = new InfoProvider(connection.getLeanClient(gameId))

    const editorApi = infoProvider.getApi()

@@ -667,27 +605,54 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange

    setEditor(editor)
    setInfoProvider(infoProvider)
+    setInfoviewApi(infoviewApi)

-    infoProvider.openPreview(editor, infoviewApi)
-    const taskgutter = new LeanTaskGutter(infoProvider.client, editor)
+    return () => { infoProvider.dispose(); editor.dispose() }
+  }, [])

-    // TODO:
-    // setRestart(() => restart)
+  const {leanClient, leanClientStarted} = useLeanClient(gameId)
+  const uriStr = `file:///${worldId}/${levelId}`
+  const uri = monaco.Uri.parse(uriStr)

-    return () => {
-      editor.dispose();
-      model.dispose();
-      abbrevRewriter.dispose();
-      taskgutter.dispose();
-      infoProvider.dispose();
-      client.dispose();
+  // Create model when level changes
+  useEffect(() => {
+    if (editor && leanClientStarted) {
+
+      let model = monaco.editor.getModel(uri)
+      if (!model) {
+        model = monaco.editor.createModel(initialCode, 'lean4', uri)
+      }
+      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
+      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
+      editor.setModel(model)
+      if (initialSelections) {
+        console.debug("Initial Selection: ", initialSelections)
+        // BUG: Somehow I get an `invalid arguments` bug here
+        // editor.setSelections(initialSelections)
+      }
+
+      return () => {
+        editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
+        model.dispose();
+      }
    }
-  }, [gameId, worldId, levelId])
+  }, [editor, levelId, connection, leanClientStarted])

-  const showRestartMessage = () => {
-    // setRestartMessage(true)
-    console.log("TODO: SHOW RESTART MESSAGE")
-  }
+
+  useEffect(() => {
+    if (editor && leanClientStarted) {
+
+      let model = monaco.editor.getModel(uri)
+      infoviewApi.serverRestarted(leanClient.initializeResult)
+
+      infoProvider.openPreview(editor, infoviewApi)
+
+      const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
+      const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
+
+      return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
+    }
+  }, [editor, connection, leanClientStarted])

  return {editor, infoProvider, editorConnection}
 }
@@ -1,55 +0,0 @@
-import * as React from 'react'
-import { Input, Typography } from '@mui/material'
-import Markdown from '../markdown'
-import Switch from '@mui/material/Switch';
-import FormControlLabel from '@mui/material/FormControlLabel';
-
-import { IMobileContext } from "../infoview/context"
-
-interface PreferencesPopupProps extends IMobileContext{
-    handleClose: () => void
-} 
-
-export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile, handleClose }: PreferencesPopupProps) {
-    return <div className="modal-wrapper">
-        <div className="modal-backdrop" onClick={handleClose} />
-        <div className="modal">
-            <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-            <Typography variant="body1" component="div" className="settings">
-                <div className='preferences-category'>
-                    <div className='category-title'>
-                        <h3>Mobile layout</h3>
-                    </div>
-                    <div className='preferences-item'>
-                        <FormControlLabel
-                            control={
-                            <Switch
-                                checked={mobile}
-                                onChange={() => setMobile(!mobile)}
-                                name="checked"
-                                color="primary"
-                            />
-                            }
-                            label="Enable"
-                            labelPlacement="start"
-                        />
-                    </div>
-                    <div className='preferences-item'>
-                        <FormControlLabel
-                            control={
-                            <Switch
-                                checked={!lockMobile}
-                                onChange={() => setLockMobile(!lockMobile)}
-                                name="checked"
-                                color="primary"
-                            />
-                            }
-                            label="Auto"
-                            labelPlacement="start"
-                        />
-                    </div>
-                </div>
-            </Typography>
-        </div>
-    </div>
-}
@@ -11,13 +11,12 @@ import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
 import { Button } from './button'
 import { MobileContext } from './infoview/context'
-import { InventoryPanel } from './inventory'
+import { InventoryOverviewPanel, InventoryPanel } from './inventory'
 import { ErasePopup } from './popup/erase'
 import { InfoPopup } from './popup/game_info'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
 import { RulesHelpPopup } from './popup/rules_help'
 import { UploadPopup } from './popup/upload'
-import { PreferencesPopup} from "./popup/preferences"
 import { WorldTreePanel } from './world_tree'

 import '../css/welcome.css'
@@ -64,7 +63,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 {mobile, setMobile, lockMobile, setLockMobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(MobileContext)
  const gameInfo = useGetGameInfoQuery({game: gameId})
  const inventory = useLoadInventoryOverviewQuery({game: gameId})

@@ -78,20 +77,15 @@ function Welcome() {
  const [info, setInfo] = React.useState(false)
  const [rulesHelp, setRulesHelp] = React.useState(false)
  const [uploadMenu, setUploadMenu] = React.useState(false)
-  const [preferencesPopup, setPreferencesPopup] = React.useState(false)
-
  function closeEraseMenu()   {setEraseMenu(false)}
  function closeImpressum()   {setImpressum(false)}
  function closeInfo()        {setInfo(false)}
  function closeRulesHelp()   {setRulesHelp(false)}
  function closeUploadMenu()  {setUploadMenu(false)}
-  function closePreferencesPopup() {setPreferencesPopup(false)}
  function toggleEraseMenu()  {setEraseMenu(!eraseMenu)}
  function toggleImpressum()  {setImpressum(!impressum)}
  function toggleInfo()       {setInfo(!info)}
  function toggleUploadMenu() {setUploadMenu(!uploadMenu)}
-  function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)}
-

  // set the window title
  useEffect(() => {
@@ -107,7 +101,7 @@ function Welcome() {
  : <>
    <WelcomeAppBar pageNumber={pageNumber} setPageNumber={setPageNumber} gameInfo={gameInfo.data} toggleImpressum={toggleImpressum}
      toggleEraseMenu={toggleEraseMenu} toggleUploadMenu={toggleUploadMenu}
-      toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
+      toggleInfo={toggleInfo} />
    <div className="app-content">
      { mobile ?
          <div className="welcome mobile">
@@ -117,7 +111,7 @@ function Welcome() {
              <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
                rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
            :
-              <InventoryPanel levelInfo={inventory?.data} />
+              <InventoryOverviewPanel data={inventory?.data} />
            )}
          </div>
        :
@@ -125,7 +119,7 @@ function Welcome() {
            <IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
            <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
              rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
-            <InventoryPanel levelInfo={inventory?.data} />
+            <InventoryOverviewPanel data={inventory?.data} />
          </Split>
      }
    </div>
@@ -134,7 +128,6 @@ function Welcome() {
    {eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
    {uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
    {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
-    {preferencesPopup ? <PreferencesPopup mobile={mobile} setMobile={setMobile} lockMobile={lockMobile} setLockMobile={setLockMobile} handleClose={closePreferencesPopup}/> : null}
  </>
 }

@@ -11,7 +11,7 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons'

 import { GameIdContext } from '../app'
-import { useAppDispatch, useMobile } from '../hooks'
+import { useAppDispatch } from '../hooks'
 import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
 import { store } from '../state/store'

@@ -197,15 +197,13 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
  const gameId = React.useContext(GameIdContext)
  const difficulty = useSelector(selectDifficulty(gameId))
  const dispatch = useAppDispatch()
-  const { mobile } = useMobile()
-

  function label(x : number) {
    return x == 0 ? 'none' : x == 1 ? 'relaxed' : 'regular'
  }


-  return <nav className={`world-selection-menu${mobile ? '' : ' desktop'}`}>
+  return <nav className="world-selection-menu">
    <div className="slider-wrap">
      <span className="difficulty-label">Rules
        <FontAwesomeIcon icon={rulesHelp ? faXmark : faCircleQuestion} className='helpButton' onClick={() => (setRulesHelp(!rulesHelp))}/>
@@ -215,7 +213,7 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
        title="Game Rules"
        min={0} max={2}
        aria-label="Game Rules"
-        value={difficulty}
+        defaultValue={difficulty}
        marks={[
          {value: 0, label: label(0)},
          {value: 1, label: label(1)},
@@ -0,0 +1,68 @@
+/**
+ *  @fileOverview todo
+ */
+
+import * as React from 'react';
+import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
+import { LeanClient } from 'lean4web/client/src/editor/leanclient';
+
+export class Connection {
+  private game: string = undefined // We only keep a connection to a single game at a time
+  private leanClient: LeanClient = null
+
+  getLeanClient(game): LeanClient {
+    if (this.game !== game) {
+      if (this.leanClient) {
+        this.leanClient.stop() // Stop previous Lean client
+      }
+      this.game = game
+      // Start a new Lean client for the new `gameId`.
+      const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + game
+      const uri = monaco.Uri.parse('file:///')
+      this.leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
+    }
+
+    return this.leanClient
+  }
+
+  /** If not already started, starts the Lean client. resolves the returned promise as soon as a
+   * Lean client is running.
+   */
+  startLeanClient = (game) => {
+    return new Promise<LeanClient>((resolve) => {
+      const leanClient = this.getLeanClient(game)
+      if (leanClient.isRunning()) {
+        resolve(leanClient)
+      } else {
+        if (!leanClient.isStarted()) {
+          leanClient.start()
+        }
+        leanClient.restarted(() => {
+          // This keep alive message is not recognized by the server,
+          // but it makes sure that the websocket connection does not
+          // time out after 60 seconds.
+          setInterval(() => {leanClient.sendNotification('$/keepAlive', {}) }, 5000)
+          resolve(leanClient)
+        })
+      }
+    })
+  }
+}
+
+export const connection = new Connection()
+
+export const ConnectionContext = React.createContext(null);
+
+export const useLeanClient = (gameId) => {
+  const leanClient = connection.getLeanClient(gameId)
+  const [leanClientStarted, setLeanClientStarted] = React.useState(leanClient.isStarted())
+
+  React.useEffect(() => {
+    const t1 = leanClient.restarted(() => { console.log("START"); setLeanClientStarted(true) })
+    const t2 = leanClient.stopped(() => { console.log("STOP"); setLeanClientStarted(false) })
+
+    return () => {t1.dispose(); t2.dispose()}
+  }, [leanClient, setLeanClientStarted])
+
+  return {leanClientStarted, leanClient}
+}
@@ -105,18 +105,11 @@ em {
  position: relative;
  flex-direction: row;
  justify-content: space-between;
-  align-items: center;
  padding: 1.1em;
  filter: drop-shadow(0 0 5px rgba(0,0,0,0.5));
  z-index: 2;
 }

-.app-bar > .app-bar-left{
-  display: flex;
-  align-items: center;
-  gap: .5em;
-}
-
 .app-bar-title, .app-bar-subtitle {
  color: white;
  font-weight: 500;
@@ -26,11 +26,7 @@
 .inventory .item {
  background: #fff;
  border: solid 1px #777;
-  padding-left: .5rem;
-  padding-right: 1.0rem;
-  padding-top: .1rem;
-  padding-bottom: .1rem;
-  position: relative;
+  padding: .1em .5em;
 }

 .inventory .item.locked {
@@ -76,21 +72,3 @@
  color: black;
  border-bottom: 0.3em solid #999;
 }
-
-
-.inventory .item .copy-button {
-	min-width: 3px;
-	min-height: 3px;
-	display: inline-block;
-	color: #ccc;
-	font-size: 0.6em;
-	padding-right: .2rem;
-	vertical-align: top;
-	position: absolute;
-	top: 0;
-	right: 0;
-	height: 100%;
-	width: 1rem;
-	align-items: end;
-	text-align: end;
-}
@@ -232,20 +232,6 @@ td code  {
  height: 100%;
 } */

-.button-row.mobile {
-  margin: .5rem;
-  padding-top: .2rem;
-}
-
-.button-row.mobile .btn {
-  padding: .5em;
-  border-radius: .2em;
-  width: 100%;
-  margin: 0;
-  text-align: center;
-}
-
-
 .typewriter-interface {
  display: flex;
  flex-flow: column;
@@ -331,6 +317,11 @@ td code  {
  margin-right: 0;
 }

+#home-btn {
+  margin-right: .5em;
+  margin-left: 0;
+}
+
 .menu.dropdown .svg-inline--fa {
  width: 1.8rem;
 }
@@ -49,6 +49,7 @@ svg .disabled {
 }

 .world-selection-menu {
+  position: absolute;
  right: 1em;
  top: 1em;
  /* margin: 1em; */
@@ -59,10 +60,6 @@ svg .disabled {
  filter: drop-shadow(4px 4px 5px rgba(0,0,0,0.5));
 }

-.world-selection-menu.desktop {
-  position: absolute;
-}
-
 .world-selection-menu .btn, .welcome .btn {
  min-width: 5em;
  text-align: center;
@@ -1,30 +1,6 @@
 import { TypedUseSelectorHook, useDispatch, useSelector } from 'react-redux'
 import type { RootState, AppDispatch } from './state/store'

-import { setMobile as setMobileState, setLockMobile as setLockMobileState} from "./state/preferences"
-
 // Use throughout your app instead of plain `useDispatch` and `useSelector`
 export const useAppDispatch: () => AppDispatch = useDispatch
 export const useAppSelector: TypedUseSelectorHook<RootState> = useSelector
-
-export const useMobile = () => {
-  const dispatch = useAppDispatch();
-
-  const mobile = useAppSelector((state) => state.preferences.mobile);
-  const lockMobile = useAppSelector((state) => state.preferences.lockMobile);
-
-  const setMobile = (val: boolean) => {
-    dispatch(setMobileState(val));
-  };
-
-  const setLockMobile = (val: boolean) => {
-    dispatch(setLockMobileState(val));
-  };
-
-  return {
-    mobile,
-    setMobile,
-    lockMobile,
-    setLockMobile,
-  };
-};
@@ -1,6 +1,7 @@
 import * as React from 'react'
 import { createRoot } from 'react-dom/client'
 import App from './app'
+import { ConnectionContext, connection } from './connection'
 import { store } from './state/store'
 import { Provider } from 'react-redux'
 import type { RouteObject } from "react-router"
@@ -9,8 +10,11 @@ import ErrorPage from './components/error_page'
 import Welcome from './components/welcome'
 import LandingPage from './components/landing_page'
 import Level from './components/level'
+import { monacoSetup } from 'lean4web/client/src/monacoSetup'


+monacoSetup()
+

 // If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to
 // `/g/local/game`. This is used for the devcontainer setup
@@ -57,7 +61,9 @@ const root = createRoot(container!);
 root.render(
  <React.StrictMode>
    <Provider store={store}>
-      <RouterProvider router={router} />
+      <ConnectionContext.Provider value={connection}>
+        <RouterProvider router={router} />
+      </ConnectionContext.Provider>
    </Provider>
  </React.StrictMode>
 );
@@ -35,7 +35,6 @@ export interface InventoryTile {
  locked: boolean,
  new: boolean,
  hidden: boolean
-  altTitle: string,
 }

 export interface LevelInfo {
@@ -72,6 +71,13 @@ interface Doc {
  category: string,
 }

+export interface WorldOverview {
+  world: string
+  tactics: InventoryTile[]
+  lemmas: InventoryTile[]
+  definitions: InventoryTile[]
+}
+
 // Define a service using a base URL and expected endpoints
 export const apiSlice = createApi({
  reducerPath: 'gameApi',
@@ -83,7 +89,7 @@ export const apiSlice = createApi({
    loadLevel: builder.query<LevelInfo, {game: string, world: string, level: number}>({
      query: ({game, world, level}) => `${game}/level__${world}__${level}.json`,
    }),
-    loadInventoryOverview: builder.query<InventoryOverview, {game: string}>({
+    loadInventoryOverview: builder.query<WorldOverview[], {game: string}>({
      query: ({game}) => `${game}/inventory.json`,
    }),
    loadDoc: builder.query<Doc, {game: string, name: string, type: "lemma"|"tactic"}>({
@@ -36,24 +36,3 @@ export async function saveState(state: any) {
    // Ignore
  }
 }
-
-const PREFERENCES_KEY = "preferences"
-
-/** Load from browser storage */
-export function loadPreferences() {
-  try {
-    const serializedState = localStorage.getItem(PREFERENCES_KEY);
-    return JSON.parse(serializedState)
-  } catch (e) {
-    return undefined;
-  }
-}
-
-export function savePreferences(state: any) {
-  try {
-    const serializedState = JSON.stringify(state)
-    localStorage.setItem(PREFERENCES_KEY, serializedState);
-  } catch (e) {
-    // Ignore
-  }
-}
@@ -1,37 +0,0 @@
-import { createSlice } from "@reduxjs/toolkit";
-
-import { loadPreferences } from "./local_storage";
-
-interface PreferencesState {
-  mobile: boolean;
-  lockMobile: boolean;
-}
-
-export function getWindowDimensions() {
-  const {innerWidth: width, innerHeight: height } = window
-  return {width, height}
-}
-
-const { width } = getWindowDimensions()
-
-export const AUTO_SWITCH_THRESHOLD = 800
-
-const initialState: PreferencesState = loadPreferences() ?? {
-    mobile: width < AUTO_SWITCH_THRESHOLD,
-    lockMobile: false
-}
-
-export const preferencesSlice = createSlice({
-  name: "preferences",
-  initialState,
-  reducers: {
-    setMobile: (state, action) => {
-      state.mobile = action.payload;
-    },
-    setLockMobile: (state, action) => {
-      state.lockMobile = action.payload;
-    },
-  },
-});
-
-export const { setMobile, setLockMobile } = preferencesSlice.actions;
@@ -7,19 +7,21 @@ import { debounce } from "debounce";
 import { connection } from '../connection'
 import { apiSlice } from './api'
 import { progressSlice } from './progress'
-import { preferencesSlice } from "./preferences"
-import { saveState, savePreferences } from "./local_storage";
+import { saveState } from "./local_storage";


 export const store = configureStore({
  reducer: {
    [apiSlice.reducerPath]: apiSlice.reducer,
    [progressSlice.name]: progressSlice.reducer,
-    [preferencesSlice.name]: preferencesSlice.reducer,
  },
  // Make connection available in thunks:
  middleware: getDefaultMiddleware =>
-    getDefaultMiddleware().concat(apiSlice.middleware),
+    getDefaultMiddleware({
+      thunk: {
+        extraArgument: { connection }
+      }
+    }).concat(apiSlice.middleware),
 });

 /**
@@ -29,7 +31,6 @@ export const store = configureStore({
 store.subscribe(
  debounce(() => {
    saveState(store.getState()[progressSlice.name]);
-    savePreferences(store.getState()[preferencesSlice.name]);
  }, 800)
 );

@@ -0,0 +1,21 @@
+import {useState, useEffect} from 'react'
+
+function getWindowDimensions() {
+  const {innerWidth: width, innerHeight: height } = window
+  return {width, height}
+}
+
+export function useWindowDimensions() {
+  const [windowDimensions, setWindowDimensions] = useState(getWindowDimensions())
+
+  useEffect(() => {
+    function handleResize() {
+      setWindowDimensions(getWindowDimensions())
+    }
+    window.addEventListener('resize', handleResize)
+    return () => window.removeEventListener('resize', handleResize)
+
+  }, [])
+
+  return windowDimensions
+}
@@ -13,10 +13,6 @@
        "@emotion/styled": "^11.10.5",
        "@fontsource/roboto": "^4.5.8",
        "@fontsource/roboto-mono": "^4.5.8",
-        "@fortawesome/fontawesome-svg-core": "^6.5.1",
-        "@fortawesome/free-regular-svg-icons": "^6.5.1",
-        "@fortawesome/free-solid-svg-icons": "^6.5.1",
-        "@fortawesome/react-fontawesome": "^0.2.0",
        "@leanprover/infoview": "^0.4.3",
        "@mui/icons-material": "^5.11.0",
        "@mui/material": "^5.11.1",
@@ -31,7 +27,7 @@
        "debounce": "^1.2.1",
        "express": "^4.18.2",
        "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-        "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
+        "lean4web": "github:hhu-adam/lean4web",
        "octokit": "^2.0.14",
        "path-browserify": "^1.0.1",
        "react": "^18.2.0",
@@ -2225,6 +2221,231 @@
      "resolved": "https://registry.npmjs.org/@emotion/weak-memoize/-/weak-memoize-0.3.1.tgz",
      "integrity": "sha512-EsBwpc7hBUJWAsNPBmJy4hxWx12v6bshQsldrVmjxJoc3isbxhOrF2IcCpaXxfvq03NwkI7sbsOLXbYuqF/8Ww=="
    },
+    "node_modules/@esbuild/android-arm": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/android-arm/-/android-arm-0.18.20.tgz",
+      "integrity": "sha512-fyi7TDI/ijKKNZTUJAQqiG5T7YjJXgnzkURqmGj13C6dCqckZBLdl4h7bkhHt/t0WP+zO9/zwroDvANaOqO5Sw==",
+      "cpu": [
+        "arm"
+      ],
+      "optional": true,
+      "os": [
+        "android"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/android-arm64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/android-arm64/-/android-arm64-0.18.20.tgz",
+      "integrity": "sha512-Nz4rJcchGDtENV0eMKUNa6L12zz2zBDXuhj/Vjh18zGqB44Bi7MBMSXjgunJgjRhCmKOjnPuZp4Mb6OKqtMHLQ==",
+      "cpu": [
+        "arm64"
+      ],
+      "optional": true,
+      "os": [
+        "android"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/android-x64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/android-x64/-/android-x64-0.18.20.tgz",
+      "integrity": "sha512-8GDdlePJA8D6zlZYJV/jnrRAi6rOiNaCC/JclcXpB+KIuvfBN4owLtgzY2bsxnx666XjJx2kDPUmnTtR8qKQUg==",
+      "cpu": [
+        "x64"
+      ],
+      "optional": true,
+      "os": [
+        "android"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/darwin-arm64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/darwin-arm64/-/darwin-arm64-0.18.20.tgz",
+      "integrity": "sha512-bxRHW5kHU38zS2lPTPOyuyTm+S+eobPUnTNkdJEfAddYgEcll4xkT8DB9d2008DtTbl7uJag2HuE5NZAZgnNEA==",
+      "cpu": [
+        "arm64"
+      ],
+      "optional": true,
+      "os": [
+        "darwin"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/darwin-x64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/darwin-x64/-/darwin-x64-0.18.20.tgz",
+      "integrity": "sha512-pc5gxlMDxzm513qPGbCbDukOdsGtKhfxD1zJKXjCCcU7ju50O7MeAZ8c4krSJcOIJGFR+qx21yMMVYwiQvyTyQ==",
+      "cpu": [
+        "x64"
+      ],
+      "optional": true,
+      "os": [
+        "darwin"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/freebsd-arm64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/freebsd-arm64/-/freebsd-arm64-0.18.20.tgz",
+      "integrity": "sha512-yqDQHy4QHevpMAaxhhIwYPMv1NECwOvIpGCZkECn8w2WFHXjEwrBn3CeNIYsibZ/iZEUemj++M26W3cNR5h+Tw==",
+      "cpu": [
+        "arm64"
+      ],
+      "optional": true,
+      "os": [
+        "freebsd"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/freebsd-x64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/freebsd-x64/-/freebsd-x64-0.18.20.tgz",
+      "integrity": "sha512-tgWRPPuQsd3RmBZwarGVHZQvtzfEBOreNuxEMKFcd5DaDn2PbBxfwLcj4+aenoh7ctXcbXmOQIn8HI6mCSw5MQ==",
+      "cpu": [
+        "x64"
+      ],
+      "optional": true,
+      "os": [
+        "freebsd"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/linux-arm": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/linux-arm/-/linux-arm-0.18.20.tgz",
+      "integrity": "sha512-/5bHkMWnq1EgKr1V+Ybz3s1hWXok7mDFUMQ4cG10AfW3wL02PSZi5kFpYKrptDsgb2WAJIvRcDm+qIvXf/apvg==",
+      "cpu": [
+        "arm"
+      ],
+      "optional": true,
+      "os": [
+        "linux"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/linux-arm64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/linux-arm64/-/linux-arm64-0.18.20.tgz",
+      "integrity": "sha512-2YbscF+UL7SQAVIpnWvYwM+3LskyDmPhe31pE7/aoTMFKKzIc9lLbyGUpmmb8a8AixOL61sQ/mFh3jEjHYFvdA==",
+      "cpu": [
+        "arm64"
+      ],
+      "optional": true,
+      "os": [
+        "linux"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/linux-ia32": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/linux-ia32/-/linux-ia32-0.18.20.tgz",
+      "integrity": "sha512-P4etWwq6IsReT0E1KHU40bOnzMHoH73aXp96Fs8TIT6z9Hu8G6+0SHSw9i2isWrD2nbx2qo5yUqACgdfVGx7TA==",
+      "cpu": [
+        "ia32"
+      ],
+      "optional": true,
+      "os": [
+        "linux"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/linux-loong64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/linux-loong64/-/linux-loong64-0.18.20.tgz",
+      "integrity": "sha512-nXW8nqBTrOpDLPgPY9uV+/1DjxoQ7DoB2N8eocyq8I9XuqJ7BiAMDMf9n1xZM9TgW0J8zrquIb/A7s3BJv7rjg==",
+      "cpu": [
+        "loong64"
+      ],
+      "optional": true,
+      "os": [
+        "linux"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/linux-mips64el": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/linux-mips64el/-/linux-mips64el-0.18.20.tgz",
+      "integrity": "sha512-d5NeaXZcHp8PzYy5VnXV3VSd2D328Zb+9dEq5HE6bw6+N86JVPExrA6O68OPwobntbNJ0pzCpUFZTo3w0GyetQ==",
+      "cpu": [
+        "mips64el"
+      ],
+      "optional": true,
+      "os": [
+        "linux"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/linux-ppc64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/linux-ppc64/-/linux-ppc64-0.18.20.tgz",
+      "integrity": "sha512-WHPyeScRNcmANnLQkq6AfyXRFr5D6N2sKgkFo2FqguP44Nw2eyDlbTdZwd9GYk98DZG9QItIiTlFLHJHjxP3FA==",
+      "cpu": [
+        "ppc64"
+      ],
+      "optional": true,
+      "os": [
+        "linux"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/linux-riscv64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/linux-riscv64/-/linux-riscv64-0.18.20.tgz",
+      "integrity": "sha512-WSxo6h5ecI5XH34KC7w5veNnKkju3zBRLEQNY7mv5mtBmrP/MjNBCAlsM2u5hDBlS3NGcTQpoBvRzqBcRtpq1A==",
+      "cpu": [
+        "riscv64"
+      ],
+      "optional": true,
+      "os": [
+        "linux"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/linux-s390x": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/linux-s390x/-/linux-s390x-0.18.20.tgz",
+      "integrity": "sha512-+8231GMs3mAEth6Ja1iK0a1sQ3ohfcpzpRLH8uuc5/KVDFneH6jtAJLFGafpzpMRO6DzJ6AvXKze9LfFMrIHVQ==",
+      "cpu": [
+        "s390x"
+      ],
+      "optional": true,
+      "os": [
+        "linux"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
    "node_modules/@esbuild/linux-x64": {
      "version": "0.18.20",
      "resolved": "https://registry.npmjs.org/@esbuild/linux-x64/-/linux-x64-0.18.20.tgz",
@@ -2240,6 +2461,96 @@
        "node": ">=12"
      }
    },
+    "node_modules/@esbuild/netbsd-x64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/netbsd-x64/-/netbsd-x64-0.18.20.tgz",
+      "integrity": "sha512-iO1c++VP6xUBUmltHZoMtCUdPlnPGdBom6IrO4gyKPFFVBKioIImVooR5I83nTew5UOYrk3gIJhbZh8X44y06A==",
+      "cpu": [
+        "x64"
+      ],
+      "optional": true,
+      "os": [
+        "netbsd"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/openbsd-x64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/openbsd-x64/-/openbsd-x64-0.18.20.tgz",
+      "integrity": "sha512-e5e4YSsuQfX4cxcygw/UCPIEP6wbIL+se3sxPdCiMbFLBWu0eiZOJ7WoD+ptCLrmjZBK1Wk7I6D/I3NglUGOxg==",
+      "cpu": [
+        "x64"
+      ],
+      "optional": true,
+      "os": [
+        "openbsd"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/sunos-x64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/sunos-x64/-/sunos-x64-0.18.20.tgz",
+      "integrity": "sha512-kDbFRFp0YpTQVVrqUd5FTYmWo45zGaXe0X8E1G/LKFC0v8x0vWrhOWSLITcCn63lmZIxfOMXtCfti/RxN/0wnQ==",
+      "cpu": [
+        "x64"
+      ],
+      "optional": true,
+      "os": [
+        "sunos"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/win32-arm64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/win32-arm64/-/win32-arm64-0.18.20.tgz",
+      "integrity": "sha512-ddYFR6ItYgoaq4v4JmQQaAI5s7npztfV4Ag6NrhiaW0RrnOXqBkgwZLofVTlq1daVTQNhtI5oieTvkRPfZrePg==",
+      "cpu": [
+        "arm64"
+      ],
+      "optional": true,
+      "os": [
+        "win32"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/win32-ia32": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/win32-ia32/-/win32-ia32-0.18.20.tgz",
+      "integrity": "sha512-Wv7QBi3ID/rROT08SABTS7eV4hX26sVduqDOTe1MvGMjNd3EjOz4b7zeexIR62GTIEKrfJXKL9LFxTYgkyeu7g==",
+      "cpu": [
+        "ia32"
+      ],
+      "optional": true,
+      "os": [
+        "win32"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
+    "node_modules/@esbuild/win32-x64": {
+      "version": "0.18.20",
+      "resolved": "https://registry.npmjs.org/@esbuild/win32-x64/-/win32-x64-0.18.20.tgz",
+      "integrity": "sha512-kTdfRcSiDfQca/y9QIkng02avJ+NCaQvrMejlsB3RRv5sE9rRoeBPISaZpKxHELzRxZyLvNts1P27W3wV+8geQ==",
+      "cpu": [
+        "x64"
+      ],
+      "optional": true,
+      "os": [
+        "win32"
+      ],
+      "engines": {
+        "node": ">=12"
+      }
+    },
    "node_modules/@floating-ui/core": {
      "version": "1.5.0",
      "resolved": "https://registry.npmjs.org/@floating-ui/core/-/core-1.5.0.tgz",
@@ -2285,45 +2596,33 @@
      "integrity": "sha512-KrJdmkqz6DszT2wV/bbhXef4r0hV3B0vw2mAqei8A2kRnvq+gcJLmmIeQ94vu9VEXrUQzos5M9lH1TAAXpRphw=="
    },
    "node_modules/@fortawesome/fontawesome-common-types": {
-      "version": "6.5.1",
-      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.5.1.tgz",
-      "integrity": "sha512-GkWzv+L6d2bI5f/Vk6ikJ9xtl7dfXtoRu3YGE6nq0p/FFqA1ebMOAWg3XgRyb0I6LYyYkiAo+3/KrwuBp8xG7A==",
+      "version": "6.4.2",
+      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.4.2.tgz",
+      "integrity": "sha512-1DgP7f+XQIJbLFCTX1V2QnxVmpLdKdzzo2k8EmvDOePfchaIGQ9eCHj2up3/jNEbZuBqel5OxiaOJf37TWauRA==",
      "hasInstallScript": true,
      "engines": {
        "node": ">=6"
      }
    },
    "node_modules/@fortawesome/fontawesome-svg-core": {
-      "version": "6.5.1",
-      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-svg-core/-/fontawesome-svg-core-6.5.1.tgz",
-      "integrity": "sha512-MfRCYlQPXoLlpem+egxjfkEuP9UQswTrlCOsknus/NcMoblTH2g0jPrapbcIb04KGA7E2GZxbAccGZfWoYgsrQ==",
+      "version": "6.4.2",
+      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-svg-core/-/fontawesome-svg-core-6.4.2.tgz",
+      "integrity": "sha512-gjYDSKv3TrM2sLTOKBc5rH9ckje8Wrwgx1CxAPbN5N3Fm4prfi7NsJVWd1jklp7i5uSCVwhZS5qlhMXqLrpAIg==",
      "hasInstallScript": true,
      "dependencies": {
-        "@fortawesome/fontawesome-common-types": "6.5.1"
-      },
-      "engines": {
-        "node": ">=6"
-      }
-    },
-    "node_modules/@fortawesome/free-regular-svg-icons": {
-      "version": "6.5.1",
-      "resolved": "https://registry.npmjs.org/@fortawesome/free-regular-svg-icons/-/free-regular-svg-icons-6.5.1.tgz",
-      "integrity": "sha512-m6ShXn+wvqEU69wSP84coxLbNl7sGVZb+Ca+XZq6k30SzuP3X4TfPqtycgUh9ASwlNh5OfQCd8pDIWxl+O+LlQ==",
-      "hasInstallScript": true,
-      "dependencies": {
-        "@fortawesome/fontawesome-common-types": "6.5.1"
+        "@fortawesome/fontawesome-common-types": "6.4.2"
      },
      "engines": {
        "node": ">=6"
      }
    },
    "node_modules/@fortawesome/free-solid-svg-icons": {
-      "version": "6.5.1",
-      "resolved": "https://registry.npmjs.org/@fortawesome/free-solid-svg-icons/-/free-solid-svg-icons-6.5.1.tgz",
-      "integrity": "sha512-S1PPfU3mIJa59biTtXJz1oI0+KAXW6bkAb31XKhxdxtuXDiUIFsih4JR1v5BbxY7hVHsD1RKq+jRkVRaf773NQ==",
+      "version": "6.4.2",
+      "resolved": "https://registry.npmjs.org/@fortawesome/free-solid-svg-icons/-/free-solid-svg-icons-6.4.2.tgz",
+      "integrity": "sha512-sYwXurXUEQS32fZz9hVCUUv/xu49PEJEyUOsA51l6PU/qVgfbTb2glsTEaJngVVT8VqBATRIdh7XVgV1JF1LkA==",
      "hasInstallScript": true,
      "dependencies": {
-        "@fortawesome/fontawesome-common-types": "6.5.1"
+        "@fortawesome/fontawesome-common-types": "6.4.2"
      },
      "engines": {
        "node": ">=6"
@@ -2539,9 +2838,9 @@
      }
    },
    "node_modules/@leanprover/infoview": {
-      "version": "0.4.4",
-      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.4.tgz",
-      "integrity": "sha512-OxHffFaHcEudLyBEWpicOl7TfXuTYxW5Sz1RkHdUINWJpQsQn60YDF5fNRKmSb0d/fm7p+LVeBvM273jvfR5wQ==",
+      "version": "0.4.3",
+      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.3.tgz",
+      "integrity": "sha512-SufdOr2myHAbZNUmobfQdAhsEC5H9ddi3KS0z1v/8riWSMm+yJk3u4LxVuzCmmSmV2QxFqtFzn5z+HQqj1Vo7g==",
      "dependencies": {
        "@leanprover/infoview-api": "~0.2.1",
        "@vscode/codicons": "^0.0.32",
@@ -4778,6 +5077,81 @@
        }
      }
    },
+    "node_modules/@swc/core-darwin-arm64": {
+      "version": "1.3.95",
+      "resolved": "https://registry.npmjs.org/@swc/core-darwin-arm64/-/core-darwin-arm64-1.3.95.tgz",
+      "integrity": "sha512-VAuBAP3MNetO/yBIBzvorUXq7lUBwhfpJxYViSxyluMwtoQDhE/XWN598TWMwMl1ZuImb56d7eUsuFdjgY7pJw==",
+      "cpu": [
+        "arm64"
+      ],
+      "optional": true,
+      "os": [
+        "darwin"
+      ],
+      "engines": {
+        "node": ">=10"
+      }
+    },
+    "node_modules/@swc/core-darwin-x64": {
+      "version": "1.3.95",
+      "resolved": "https://registry.npmjs.org/@swc/core-darwin-x64/-/core-darwin-x64-1.3.95.tgz",
+      "integrity": "sha512-20vF2rvUsN98zGLZc+dsEdHvLoCuiYq/1B+TDeE4oolgTFDmI1jKO+m44PzWjYtKGU9QR95sZ6r/uec0QC5O4Q==",
+      "cpu": [
+        "x64"
+      ],
+      "optional": true,
+      "os": [
+        "darwin"
+      ],
+      "engines": {
+        "node": ">=10"
+      }
+    },
+    "node_modules/@swc/core-linux-arm-gnueabihf": {
+      "version": "1.3.95",
+      "resolved": "https://registry.npmjs.org/@swc/core-linux-arm-gnueabihf/-/core-linux-arm-gnueabihf-1.3.95.tgz",
+      "integrity": "sha512-oEudEM8PST1MRNGs+zu0cx5i9uP8TsLE4/L9HHrS07Ck0RJ3DCj3O2fU832nmLe2QxnAGPwBpSO9FntLfOiWEQ==",
+      "cpu": [
+        "arm"
+      ],
+      "optional": true,
+      "os": [
+        "linux"
+      ],
+      "engines": {
+        "node": ">=10"
+      }
+    },
+    "node_modules/@swc/core-linux-arm64-gnu": {
+      "version": "1.3.95",
+      "resolved": "https://registry.npmjs.org/@swc/core-linux-arm64-gnu/-/core-linux-arm64-gnu-1.3.95.tgz",
+      "integrity": "sha512-pIhFI+cuC1aYg+0NAPxwT/VRb32f2ia8oGxUjQR6aJg65gLkUYQzdwuUmpMtFR2WVf7WVFYxUnjo4UyMuyh3ng==",
+      "cpu": [
+        "arm64"
+      ],
+      "optional": true,
+      "os": [
+        "linux"
+      ],
+      "engines": {
+        "node": ">=10"
+      }
+    },
+    "node_modules/@swc/core-linux-arm64-musl": {
+      "version": "1.3.95",
+      "resolved": "https://registry.npmjs.org/@swc/core-linux-arm64-musl/-/core-linux-arm64-musl-1.3.95.tgz",
+      "integrity": "sha512-ZpbTr+QZDT4OPJfjPAmScqdKKaT+wGurvMU5AhxLaf85DuL8HwUwwlL0n1oLieLc47DwIJEMuKQkYhXMqmJHlg==",
+      "cpu": [
+        "arm64"
+      ],
+      "optional": true,
+      "os": [
+        "linux"
+      ],
+      "engines": {
+        "node": ">=10"
+      }
+    },
    "node_modules/@swc/core-linux-x64-gnu": {
      "version": "1.3.95",
      "resolved": "https://registry.npmjs.org/@swc/core-linux-x64-gnu/-/core-linux-x64-gnu-1.3.95.tgz",
@@ -4808,6 +5182,51 @@
        "node": ">=10"
      }
    },
+    "node_modules/@swc/core-win32-arm64-msvc": {
+      "version": "1.3.95",
+      "resolved": "https://registry.npmjs.org/@swc/core-win32-arm64-msvc/-/core-win32-arm64-msvc-1.3.95.tgz",
+      "integrity": "sha512-YaP4x/aZbUyNdqCBpC2zL8b8n58MEpOUpmOIZK6G1SxGi+2ENht7gs7+iXpWPc0sy7X3YPKmSWMAuui0h8lgAA==",
+      "cpu": [
+        "arm64"
+      ],
+      "optional": true,
+      "os": [
+        "win32"
+      ],
+      "engines": {
+        "node": ">=10"
+      }
+    },
+    "node_modules/@swc/core-win32-ia32-msvc": {
+      "version": "1.3.95",
+      "resolved": "https://registry.npmjs.org/@swc/core-win32-ia32-msvc/-/core-win32-ia32-msvc-1.3.95.tgz",
+      "integrity": "sha512-w0u3HI916zT4BC/57gOd+AwAEjXeUlQbGJ9H4p/gzs1zkSHtoDQghVUNy3n/ZKp9KFod/95cA8mbVF9t1+6epQ==",
+      "cpu": [
+        "ia32"
+      ],
+      "optional": true,
+      "os": [
+        "win32"
+      ],
+      "engines": {
+        "node": ">=10"
+      }
+    },
+    "node_modules/@swc/core-win32-x64-msvc": {
+      "version": "1.3.95",
+      "resolved": "https://registry.npmjs.org/@swc/core-win32-x64-msvc/-/core-win32-x64-msvc-1.3.95.tgz",
+      "integrity": "sha512-5RGnMt0S6gg4Gc6QtPUJ3Qs9Un4sKqccEzgH/tj7V/DVTJwKdnBKxFZfgQ34OR2Zpz7zGOn889xwsFVXspVWNA==",
+      "cpu": [
+        "x64"
+      ],
+      "optional": true,
+      "os": [
+        "win32"
+      ],
+      "engines": {
+        "node": ">=10"
+      }
+    },
    "node_modules/@swc/counter": {
      "version": "0.1.2",
      "resolved": "https://registry.npmjs.org/@swc/counter/-/counter-0.1.2.tgz",
@@ -8116,6 +8535,19 @@
      "resolved": "https://registry.npmjs.org/fs.realpath/-/fs.realpath-1.0.0.tgz",
      "integrity": "sha512-OO0pH2lK6a0hZnAdau5ItzHPI6pUlvI7jMVnxUQRtw4owF2wk8lOSabtGDCTP4Ggrg2MbGnWO9X8K1t4+fGMDw=="
    },
+    "node_modules/fsevents": {
+      "version": "2.3.3",
+      "resolved": "https://registry.npmjs.org/fsevents/-/fsevents-2.3.3.tgz",
+      "integrity": "sha512-5xoDfX+fL7faATnagmWPpbFtwh/R77WmMMqqHGS65C3vvB0YHrgF+B1YmZ3441tMj5n63k0212XNoJwzlhffQw==",
+      "hasInstallScript": true,
+      "optional": true,
+      "os": [
+        "darwin"
+      ],
+      "engines": {
+        "node": "^8.16.0 || ^10.6.0 || >=11.0.0"
+      }
+    },
    "node_modules/function-bind": {
      "version": "1.1.1",
      "resolved": "https://registry.npmjs.org/function-bind/-/function-bind-1.1.1.tgz",
@@ -10081,8 +10513,7 @@
    },
    "node_modules/lean4web": {
      "version": "0.1.0",
-      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
-      "integrity": "sha512-s9qYeXuMNBGDPKC5IuFTjV/j8tQCRkZr+poYKEWljrM95rsz4JHIvjdEt891fE9JhPDLSN+iXNRXwIOCT6FlMg==",
+      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#6fc9c11179934cce7ca1f78140c57b6931186b42",
      "dependencies": {
        "@emotion/react": "^11.11.1",
        "@emotion/styled": "^11.11.0",
@@ -10091,7 +10522,7 @@
        "@fortawesome/fontawesome-svg-core": "^6.2.0",
        "@fortawesome/free-solid-svg-icons": "^6.2.0",
        "@fortawesome/react-fontawesome": "^0.2.0",
-        "@leanprover/infoview": "^0.4.4",
+        "@leanprover/infoview": "^0.4.3",
        "@mui/material": "^5.13.7",
        "@vitejs/plugin-react-swc": "^3.4.0",
        "express": "^4.18.2",
@@ -10,10 +10,6 @@
    "@emotion/styled": "^11.10.5",
    "@fontsource/roboto": "^4.5.8",
    "@fontsource/roboto-mono": "^4.5.8",
-    "@fortawesome/fontawesome-svg-core": "^6.5.1",
-    "@fortawesome/free-regular-svg-icons": "^6.5.1",
-    "@fortawesome/free-solid-svg-icons": "^6.5.1",
-    "@fortawesome/react-fontawesome": "^0.2.0",
    "@leanprover/infoview": "^0.4.3",
    "@mui/icons-material": "^5.11.0",
    "@mui/material": "^5.11.1",
@@ -28,7 +24,7 @@
    "debounce": "^1.2.1",
    "express": "^4.18.2",
    "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-    "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
+    "lean4web": "github:hhu-adam/lean4web",
    "octokit": "^2.0.14",
    "path-browserify": "^1.0.1",
    "react": "^18.2.0",
@@ -1,6 +1,5 @@
 #/bin/bash

-# Note: This fails if there is no default toolchain installed
 ELAN_HOME=$(lake env printenv ELAN_HOME)

 # $1 : the game directory
@@ -1,12 +1,23 @@
-import GameServer.Helpers
-import GameServer.Inventory
-import GameServer.Options
-import GameServer.SaveData
+import GameServer.EnvExtensions

 open Lean Meta Elab Command

 set_option autoImplicit false

+/-- Let `MakeGame` print the reasons why the worlds depend on each other. -/
+register_option lean4game.showDependencyReasons : Bool := {
+  defValue := false
+  descr := "show reasons for calculated world dependencies."
+}
+
+/-- Let `MakeGame` print the reasons why the worlds depend on each other.
+
+Note: currently unused in favour of setting `set_option trace.debug true`. -/
+register_option lean4game.verbose : Bool := {
+  defValue := false
+  descr := "display more info messages to help developing the game."
+}
+
 /-! # Game metadata -/

 /-- Switch to the specified `Game` (and create it if non-existent). Example: `Game "NNG"` -/
@@ -41,15 +52,13 @@ elab "Title" t:str : command => do

 /-- Define the introduction of the current game/world/level. -/
 elab "Introduction" t:str : command => do
-  let intro := t.getString
  match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with introduction := intro}
-  | .World => modifyCurWorld  fun world => pure {world with introduction := intro}
-  | .Game => modifyCurGame  fun game => pure {game with introduction := intro}
+  | .Level => modifyCurLevel fun level => pure {level with introduction := t.getString}
+  | .World => modifyCurWorld  fun world => pure {world with introduction := t.getString}
+  | .Game => modifyCurGame  fun game => pure {game with introduction := t.getString}

 /-- Define the info of the current game. Used for e.g. credits -/
 elab "Info" t:str : command => do
-  let info:= t.getString
  match ← getCurLayer with
  | .Level =>
    logError "Can't use `Info` in a level!"
@@ -57,7 +66,7 @@ elab "Info" t:str : command => do
  | .World =>
    logError "Can't use `Info` in a world"
    pure ()
-  | .Game => modifyCurGame  fun game => pure {game with info := info}
+  | .Game => modifyCurGame  fun game => pure {game with info := t.getString}

 /-- Provide the location of the image for the current game/world/level.
 Paths are relative to the lean project's root. -/
@@ -81,11 +90,10 @@ elab "Image" t:str : command => do
 /-- Define the conclusion of the current game or current level if some
 building a level. -/
 elab "Conclusion" t:str : command => do
-  let conclusion := t.getString
  match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with conclusion := conclusion}
-  | .World => modifyCurWorld  fun world => pure {world with conclusion := conclusion}
-  | .Game => modifyCurGame  fun game => pure {game with conclusion := conclusion}
+  | .Level => modifyCurLevel fun level => pure {level with conclusion := t.getString}
+  | .World => modifyCurWorld  fun world => pure {world with conclusion := t.getString}
+  | .Game => modifyCurGame  fun game => pure {game with conclusion := t.getString}

 /-- A list of games that should be played before this one. Example `Prerequisites "NNG" "STG"`. -/
 elab "Prerequisites" t:str* : command => do
@@ -94,15 +102,13 @@ elab "Prerequisites" t:str* : command => do

 /-- Short caption for the game (1 sentence) -/
 elab "CaptionShort" t:str : command => do
-  let caption := t.getString
  modifyCurGame fun game => pure {game with
-    tile := {game.tile with short := caption}}
+    tile := {game.tile with short := t.getString}}

 /-- More detailed description what the game is about (2-4 sentences). -/
 elab "CaptionLong" t:str : command => do
-  let caption := t.getString
  modifyCurGame fun game => pure {game with
-    tile := {game.tile with long := caption}}
+    tile := {game.tile with long := t.getString}}

 /-- A list of Languages the game is translated to. For example `Languages "German" "English"`.
 NOTE: For the time being, only a single language is supported.
@@ -124,12 +130,119 @@ elab "CoverImage" t:str : command => do

 /-! # Inventory

-The inventory contains docs for tactics, theorems, and definitions. These are all locked
+The inventory contains docs for tactics, lemmas, and definitions. These are all locked
 in the first level and get enabled during the game.
 -/

 /-! ## Doc entries -/

+/-- Copied from `Mathlib.Tactic.HelpCmd`.
+
+Gets the initial string token in a parser description. For example, for a declaration like
+`syntax "bla" "baz" term : tactic`, it returns `some "bla"`. Returns `none` for syntax declarations
+that don't start with a string constant. -/
+partial def getHeadTk (e : Expr) : Option String :=
+  match (Expr.withApp e λ e a => (e.constName?.getD Name.anonymous, a)) with
+  | (``ParserDescr.node, #[_, _, p]) => getHeadTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getHeadTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getHeadTk p
+  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getHeadTk p
+  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
+  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => some tk
+  | (``Parser.withAntiquot, #[_, p]) => getHeadTk p
+  | (``Parser.leadingNode, #[_, _, p]) => getHeadTk p
+  | (``HAndThen.hAndThen, #[_, _, _, _, p, _]) => getHeadTk p
+  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
+  | (``Parser.symbol, #[.lit (.strVal tk)]) => some tk
+  | _ => none
+
+/-- Modified from `#help` in `Mathlib.Tactic.HelpCmd` -/
+def getTacticDocstring (env : Environment) (name: Name) : CommandElabM (Option String) := do
+  let name := name.toString (escape := false)
+  let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {}
+
+  let catName : Name := `tactic
+  let catStx : Ident := mkIdent catName -- TODO
+  let some cat := (Parser.parserExtension.getState env).categories.find? catName
+    | throwErrorAt catStx "{catStx} is not a syntax category"
+  liftTermElabM <| Term.addCategoryInfo catStx catName
+  for (k, _) in cat.kinds do
+    let mut used := false
+    if let some tk := do getHeadTk (← (← env.find? k).value?) then
+      let tk := tk.trim
+      if name ≠ tk then -- was `!name.isPrefixOf tk`
+        continue
+      used := true
+      decls := decls.insert tk ((decls.findD tk #[]).push k)
+  for (_name, ks) in decls do
+    for k in ks do
+      if let some doc ← findDocString? env k then
+        return doc
+
+  logWarning <| m!"Could not find a docstring for tactic {name}, consider adding one " ++
+    m!"using `TacticDoc {name} \"some doc\"`"
+  return none
+
+/-- Retrieve the docstring associated to an inventory item. For Tactics, this
+is not guaranteed to work. -/
+def getDocstring (env : Environment) (name : Name) (type : InventoryType) :
+    CommandElabM (Option String) :=
+  match type with
+  -- for tactics it's a lookup following mathlib's `#help`. not guaranteed to be the correct one.
+  | .Tactic => getTacticDocstring env name
+  | .Lemma => findDocString? env name
+  -- TODO: for definitions not implemented yet, does it work?
+  | .Definition => findDocString? env name
+
+/-- Checks if `inventoryTemplateExt` contains an entry with `(type, name)` and yields
+a warning otherwise. If `template` is provided, it will add such an entry instead of yielding a
+warning.
+
+`ref` is the syntax piece. If `name` is not provided, it will use `ident.getId`.
+I used this workaround, because I needed a new name (with correct namespace etc)
+to be used, and I don't know how to create a new ident with same position but different name.
+-/
+def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.getId)
+    (template : Option String := none) : CommandElabM Unit := do
+  -- note: `name` is an `Ident` (instead of `Name`) for the log messages.
+  let env ← getEnv
+  let n := name
+  -- Find a key with matching `(type, name)`.
+  match (inventoryTemplateExt.getState env).findIdx?
+    (fun x => x.name == n && x.type == type) with
+  -- Nothing to do if the entry exists
+  | some _ => pure ()
+  | none =>
+    match template with
+    -- Warn about missing documentation
+    | none =>
+      let docstring ← match (← getDocstring env name type) with
+      | some ds =>
+        logInfoAt ref (m!"Missing {type} Documentation. Using existing docstring. " ++
+        m!"Add {name}\nAdd `{type}Doc {name}` somewhere above this statement.")
+        pure s!"*(lean docstring)*\\\n{ds}"
+      | none =>
+        logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
+        m!"somewhere above this statement.")
+        pure "(missing)"
+
+      -- We just add a dummy entry
+      modifyEnv (inventoryTemplateExt.addEntry · {
+        type := type
+        name := name
+        category := if type == .Lemma then s!"{n.getPrefix}" else ""
+        content := docstring})
+    -- Add the default documentation
+    | some s =>
+      modifyEnv (inventoryTemplateExt.addEntry · {
+        type := type
+        name := name
+        category := if type == .Lemma then s!"{n.getPrefix}" else ""
+        content := s })
+      logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++
+        m!"docstring) instead. If you want to write a different description, add " ++
+        m!"`{type}Doc {name}` somewhere above this statement.")
+
 /-- Documentation entry of a tactic. Example:

 ```
@@ -139,40 +252,37 @@ TacticDoc rw "`rw` stands for rewrite, etc. "
 * The identifier is the tactics name. Some need to be escaped like `«have»`.
 * The description is a string supporting Markdown.
 -/
-elab doc:docComment ? "TacticDoc" name:ident content:str ? : command => do
-  let doc ← parseDocCommentLegacy doc content
+elab "TacticDoc" name:ident content:str : command =>
  modifyEnv (inventoryTemplateExt.addEntry · {
    type := .Tactic
    name := name.getId
    displayName := name.getId.toString
-    content := doc })
+    content := content.getString })

-/-- Documentation entry of a theorem. Example:
+/-- Documentation entry of a lemma. Example:

 ```
-TheoremDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
+LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 ```

-* The first identifier is used in the commands `[New/Only/Disabled]Theorem`.
-  It is preferably the true name of the theorem. However, this is not required.
+* The first identifier is used in the commands `[New/Only/Disabled]Lemma`.
+  It is preferably the true name of the lemma. However, this is not required.
 * The string following `as` is the displayed name (in the Inventory).
-* The identifier after `in` is the category to group theorems by (in the Inventory).
+* The identifier after `in` is the category to group lemmas by (in the Inventory).
 * The description is a string supporting Markdown.

 Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
-The theorem/definition to have the same fully qualified name as in mathlib.
+The lemma/definition to have the same fully qualified name as in mathlib.
 -/
-elab doc:docComment ? "TheoremDoc" name:ident "as" displayName:str "in" category:str content:str ? :
-    command => do
-  let doc ← parseDocCommentLegacy doc content
+elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
  modifyEnv (inventoryTemplateExt.addEntry · {
    type := .Lemma
    name := name.getId
    category := category.getString
    displayName := displayName.getString
-    content := doc })
+    content := content.getString })
 -- TODO: Catch the following behaviour.
-- 1. if `TheoremDoc` appears in the same file as `Statement`, it will silently use
+-- 1. if `LemmaDoc` appears in the same file as `Statement`, it will silently use
 -- it but display the info that it wasn't found in `Statement`
 -- 2. if it appears in a later file, however, it will silently not do anything and keep
 -- the first one.
@@ -190,25 +300,37 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur
 * The description is a string supporting Markdown.

 Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
-The theorem/definition to have the same fully qualified name as in mathlib.
+The lemma/definition to have the same fully qualified name as in mathlib.
 -/
-elab doc:docComment ? "DefinitionDoc" name:ident "as" displayName:str template:str ? : command => do
-  let doc ← parseDocCommentLegacy doc template
+elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
  modifyEnv (inventoryTemplateExt.addEntry · {
    type := .Definition
    name := name.getId,
    displayName := displayName.getString,
-    content := doc })
+    content := template.getString })

 /-! ## Add inventory items -/

-def checkCommandNotDuplicated (items : Array Name) (cmd := "Command") : CommandElabM Unit := do
-  if ¬ items.isEmpty then
-    logWarning s!"You should only use one `{cmd}` per level, but it takes multiple arguments: `{cmd} obj₁ obj₂ obj₃`!"
+def getStatement (name : Name) : CommandElabM MessageData := do
+  return ← addMessageContextPartial (.ofPPFormat { pp := fun
+    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
+    | none     => return "that's a bug." })
+
+-- Note: We use `String` because we can't send `MessageData` as json, but
+-- `MessageData` might be better for interactive highlighting.
+/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`.
+
+Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
+`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
+def getStatementString (name : Name) : CommandElabM String := do
+  try
+    return ← (← getStatement name).toString
+  catch
+  | _ => throwError m!"Could not find {name} in context."
+  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.

 /-- Declare tactics that are introduced by this level. -/
 elab "NewTactic" args:ident* : command => do
-  checkCommandNotDuplicated ((←getCurLevel).tactics.new) "NewTactic"
  for name in ↑args do
    checkInventoryDoc .Tactic name -- TODO: Add (template := "[docstring]")
  modifyCurLevel fun level => pure {level with
@@ -216,16 +338,14 @@ elab "NewTactic" args:ident* : command => do

 /-- Declare tactics that are introduced by this level but do not show up in inventory. -/
 elab "NewHiddenTactic" args:ident* : command => do
-  checkCommandNotDuplicated ((←getCurLevel).tactics.hidden) "NewHiddenTactic"
  for name in ↑args do
    checkInventoryDoc .Tactic name (template := "")
  modifyCurLevel fun level => pure {level with
    tactics := {level.tactics with new := level.tactics.new ++ args.map (·.getId),
                                   hidden := level.tactics.hidden ++ args.map (·.getId)}}

-/-- Declare theorems that are introduced by this level. -/
-elab "NewTheorem" args:ident* : command => do
-  checkCommandNotDuplicated ((←getCurLevel).lemmas.new) "NewTheorem"
+/-- Declare lemmas that are introduced by this level. -/
+elab "NewLemma" args:ident* : command => do
  for name in ↑args do
    try let _decl ← getConstInfo name.getId catch
      | _ => logErrorAt name m!"unknown identifier '{name}'."
@@ -235,7 +355,6 @@ elab "NewTheorem" args:ident* : command => do

 /-- Declare definitions that are introduced by this level. -/
 elab "NewDefinition" args:ident* : command => do
-  checkCommandNotDuplicated ((←getCurLevel).definitions.new) "NewDefinition"
  for name in ↑args do checkInventoryDoc .Definition name -- TODO: Add (template := "[mathlib]")
  modifyCurLevel fun level => pure {level with
    definitions := {level.definitions with new := args.map (·.getId)}}
@@ -243,36 +362,31 @@ elab "NewDefinition" args:ident* : command => do
 /-- Declare tactics that are temporarily disabled in this level.
 This is ignored if `OnlyTactic` is set. -/
 elab "DisabledTactic" args:ident* : command => do
-  checkCommandNotDuplicated ((←getCurLevel).tactics.disabled) "DisabledTactic"
  for name in ↑args do checkInventoryDoc .Tactic name
  modifyCurLevel fun level => pure {level with
    tactics := {level.tactics with disabled := args.map (·.getId)}}

-/-- Declare theorems that are temporarily disabled in this level.
-This is ignored if `OnlyTheorem` is set. -/
-elab "DisabledTheorem" args:ident* : command => do
-  checkCommandNotDuplicated ((←getCurLevel).lemmas.disabled) "DisabledTheorem"
+/-- Declare lemmas that are temporarily disabled in this level.
+This is ignored if `OnlyLemma` is set. -/
+elab "DisabledLemma" args:ident* : command => do
  for name in ↑args  do checkInventoryDoc .Lemma name
  modifyCurLevel fun level => pure {level with
    lemmas := {level.lemmas with disabled := args.map (·.getId)}}

 /-- Declare definitions that are temporarily disabled in this level -/
 elab "DisabledDefinition" args:ident* : command => do
-  checkCommandNotDuplicated ((←getCurLevel).definitions.disabled) "DisabledDefinition"
  for name in ↑args do checkInventoryDoc .Definition name
  modifyCurLevel fun level => pure {level with
    definitions := {level.definitions with disabled := args.map (·.getId)}}

 /-- Temporarily disable all tactics except the ones declared here -/
 elab "OnlyTactic" args:ident* : command => do
-  checkCommandNotDuplicated ((←getCurLevel).tactics.only) "OnlyTactic"
  for name in ↑args do checkInventoryDoc .Tactic name
  modifyCurLevel fun level => pure {level with
    tactics := {level.tactics with only := args.map (·.getId)}}

-/-- Temporarily disable all theorems except the ones declared here -/
-elab "OnlyTheorem" args:ident* : command => do
-  checkCommandNotDuplicated ((←getCurLevel).lemmas.only) "OnlyTheorem"
+/-- Temporarily disable all lemmas except the ones declared here -/
+elab "OnlyLemma" args:ident* : command => do
  for name in ↑args do checkInventoryDoc .Lemma name
  modifyCurLevel fun level => pure {level with
    lemmas := {level.lemmas with only := args.map (·.getId)}}
@@ -280,66 +394,65 @@ elab "OnlyTheorem" args:ident* : command => do
 /-- Temporarily disable all definitions except the ones declared here.
 This is ignored if `OnlyDefinition` is set. -/
 elab "OnlyDefinition" args:ident* : command => do
-  checkCommandNotDuplicated ((←getCurLevel).definitions.only) "OnlyDefinition"
  for name in ↑args do checkInventoryDoc .Definition name
  modifyCurLevel fun level => pure {level with
    definitions := {level.definitions with only := args.map (·.getId)}}

-/-- Define which tab of Lemmas is opened by default. Usage: `TheoremTab "Nat"`.
+/-- Define which tab of Lemmas is opened by default. Usage: `LemmaTab "Nat"`.
 If omitted, the current tab will remain open. -/
-elab "TheoremTab"  category:str : command =>
-  modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
-
-
-/-! DEPRECATED -/
-
-elab doc:docComment ? "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str ? :
-    command => do
-  logWarning "Deprecated. Has been renamed to `TheoremDoc`"
-  let doc ← parseDocCommentLegacy doc content
-  modifyEnv (inventoryTemplateExt.addEntry · {
-    type := .Lemma
-    name := name.getId
-    category := category.getString
-    displayName := displayName.getString
-    content := doc })
-
-elab "NewLemma" args:ident* : command => do
-  logWarning "Deprecated. Has been renamed to `NewTheorem`"
-  checkCommandNotDuplicated ((←getCurLevel).lemmas.new) "NewLemma"
-  for name in ↑args do
-    try let _decl ← getConstInfo name.getId catch
-      | _ => logErrorAt name m!"unknown identifier '{name}'."
-    checkInventoryDoc .Lemma name -- TODO: Add (template := "[mathlib]")
-  modifyCurLevel fun level => pure {level with
-    lemmas := {level.lemmas with new := args.map (·.getId)}}
-
-elab "DisabledLemma" args:ident* : command => do
-  logWarning "Deprecated. Has been renamed to `DisabledTheorem`"
-  checkCommandNotDuplicated ((←getCurLevel).lemmas.disabled) "DisabledLemma"
-  for name in ↑args  do checkInventoryDoc .Lemma name
-  modifyCurLevel fun level => pure {level with
-    lemmas := {level.lemmas with disabled := args.map (·.getId)}}
-
-elab "OnlyLemma" args:ident* : command => do
-  logWarning "Deprecated. Has been renamed to `OnlyTheorem`"
-  checkCommandNotDuplicated ((←getCurLevel).lemmas.only) "OnlyLemma"
-  for name in ↑args do checkInventoryDoc .Lemma name
-  modifyCurLevel fun level => pure {level with
-    lemmas := {level.lemmas with only := args.map (·.getId)}}
-
-elab "LemmaTab"  category:str : command => do
-  logWarning "Deprecated. Has been renamed to `TheoremTab`"
+elab "LemmaTab"  category:str : command =>
  modifyCurLevel fun level => pure {level with lemmaTab := category.getString}

 /-! # Exercise Statement -/

+/-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
+syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
+-- TODO
+
+-- TODO: Reuse the following code for checking available tactics in user code:
+structure UsedInventory where
+(tactics : HashSet Name := {})
+(definitions : HashSet Name := {})
+(lemmas : HashSet Name := {})
+
+partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : CommandElabM UsedInventory := do
+  match stx with
+  | .missing => return acc
+  | .node _info kind args =>
+    if kind == `GameServer.Tactic.Hint || kind == `GameServer.Tactic.Branch then return acc
+    return ← args.foldlM (fun acc arg => collectUsedInventory arg acc) acc
+  | .atom _info val =>
+    -- ignore syntax elements that do not start with a letter
+    -- and ignore some standard keywords
+    let allowed := ["with", "fun", "at", "only", "by"]
+    if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
+      let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
+      return {acc with tactics := acc.tactics.insert val}
+    else
+      return acc
+  | .ident _info _rawVal val _preresolved =>
+      let ns ←
+        try resolveGlobalConst (mkIdent val)
+        catch | _ => pure [] -- catch "unknown constant" error
+      return ← ns.foldlM (fun acc n => do
+        if let some (.thmInfo ..) := (← getEnv).find? n then
+          return {acc with lemmas := acc.lemmas.insertMany ns}
+        else
+          return {acc with definitions := acc.definitions.insertMany ns}
+      ) acc
+
+-- #check expandOptDocComment?
+
 /-- Define the statement of the current level. -/
 elab doc:docComment ? attrs:Parser.Term.attributes ?
    "Statement" statementName:ident ? sig:declSig val:declVal : command => do
  let lvlIdx ← getCurLevelIdx

-  let docContent ← parseDocComment doc
+  let docContent : Option String := match doc with
+  | none => none
+  | some s => match s.raw[1] with
+    | .atom _ val => val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩))
+    | _           => none --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}"

  -- Save the messages before evaluation of the proof.
  let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
@@ -440,6 +553,23 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?

 /-! # Hints -/

+syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
+
+/-- Remove any spaces at the beginning of a new line -/
+partial def removeIndentation (s : String) : String :=
+  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
+    let c := s.get i
+    let i := s.next i
+    if s.atEnd i then
+      acc.push c
+    else if removeSpaces && c == ' ' then
+      loop i acc (removeSpaces := true)
+    else if c == '\n' then
+      loop i (acc.push c) (removeSpaces := true)
+    else
+      loop i (acc.push c)
+  loop ⟨0⟩ ""
+
 /-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
 see hints. The tactic does not affect the goal state.
 -/
@@ -553,6 +683,26 @@ elab "Template" tacs:tacticSeq : tactic => do
    return {level with template := s!"{template}"}


+
+open IO.FS System FilePath in
+/-- Copies the folder `images/` to `.lake/gamedata/images/` -/
+def copyImages : IO Unit := do
+  let target : FilePath := ".lake" / "gamedata"
+  if ← FilePath.pathExists "images" then
+    for file in ← walkDir "images" do
+      let outFile := target.join file
+      -- create the directories
+      if ← file.isDir then
+        createDirAll outFile
+      else
+        if let some parent := outFile.parent then
+          createDirAll parent
+        -- copy file
+        let content ← readBinFile file
+        writeBinFile outFile content
+
+
+
 -- TODO: Notes for testing if a declaration has the simp attribute

 -- -- Test: From zulip
@@ -571,6 +721,139 @@ elab "Template" tacs:tacticSeq : tactic => do

 /-! # Make Game -/

+#eval IO.FS.createDirAll ".lake/gamedata/"
+
+-- TODO: register all of this as ToJson instance?
+def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do
+  let game ← getCurGame
+  let env ← getEnv
+  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
+
+  if ← path.isDir then
+    IO.FS.removeDirAll path
+  IO.FS.createDirAll path
+
+  -- copy the images folder
+  copyImages
+
+  for (worldId, world) in game.worlds.nodes.toArray do
+    for (levelId, level) in world.levels.toArray do
+      IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
+
+  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
+
+  for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
+    for name in allItemsByType.findD inventoryType {} do
+      let some item ← getInventoryItem? name inventoryType
+        | throwError "Expected item to exist: {name}"
+      IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
+
+  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
+    (allItemsByType.findD type {}).toArray.mapM (fun name => do
+      let some item ← getInventoryItem? name type
+        | throwError "Expected item to exist: {name}"
+      return item.toTile)
+  let inventory : InventoryOverview := {
+    lemmas := ← getTiles .Lemma
+    tactics := ← getTiles .Tactic
+    definitions := ← getTiles .Definition
+    lemmaTab := none
+  }
+  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))
+
+
+def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
+| .Tactic => level.tactics
+| .Definition => level.definitions
+| .Lemma => level.lemmas
+
+def GameLevel.setComputedInventory (level : GameLevel) :
+    InventoryType → Array InventoryTile → GameLevel
+| .Tactic, v =>     {level with tactics     := {level.tactics     with tiles := v}}
+| .Definition, v => {level with definitions := {level.definitions with tiles := v}}
+| .Lemma, v =>      {level with lemmas      := {level.lemmas      with tiles := v}}
+
+partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name))
+      (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) :
+    HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do
+  match (newArrows.find? id, decendants.find? id) with
+  | (some _, some _) => return (newArrows, decendants)
+  | _ =>
+    let mut newArr := newArrows
+    let mut desc := decendants
+    desc := desc.insert id {} -- mark as worked in case of loops
+    newArr := newArr.insert id {} -- mark as worked in case of loops
+    let children := arrows.findD id {}
+    let mut trimmedChildren := children
+    let mut theseDescs := children
+    for child in children do
+      (newArr, desc) := removeTransitiveAux child arrows newArr desc
+      let childDescs := desc.findD child {}
+      theseDescs := theseDescs.insertMany childDescs
+      for d in childDescs do
+        trimmedChildren := trimmedChildren.erase d
+    desc := desc.insert id theseDescs
+    newArr := newArr.insert id trimmedChildren
+    return (newArr, desc)
+
+def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do
+  let mut newArr := {}
+  let mut desc := {}
+  for id in arrows.toArray.map Prod.fst do
+    (newArr, desc) := removeTransitiveAux id arrows newArr desc
+    if (desc.findD id {}).contains id then
+      logError <| m!"Loop at {id}. " ++
+        m!"This should not happen and probably means that `findLoops` has a bug."
+      -- DEBUG:
+      -- for ⟨x, hx⟩ in desc.toList do
+      --   m := m ++ m!"{x}: {hx.toList}\n"
+      -- logError m
+
+  return newArr
+
+/-- The recursive part of `findLoops`. Finds loops that appear as successors of `node`.
+
+For performance reason it returns a HashSet of visited
+nodes as well. This is filled with all nodes ever looked at as they cannot be
+part of a loop anymore. -/
+partial def findLoopsAux (arrows : HashMap Name (HashSet Name)) (node : Name)
+    (path : Array Name := #[]) (visited : HashSet Name := {}) :
+    Array Name × HashSet Name := Id.run do
+  let mut visited := visited
+  match path.getIdx? node with
+  | some i =>
+    -- Found a loop: `node` is already the iᵗʰ element of the path
+    return (path.extract i path.size, visited.insert node)
+  | none =>
+    for successor in arrows.findD node {} do
+      -- If we already visited the successor, it cannot be part of a loop anymore
+      if visited.contains successor then
+        continue
+      -- Find any loop involving `successor`
+      let (loop, _) := findLoopsAux arrows successor (path.push node) visited
+      visited := visited.insert successor
+      -- No loop found in the dependants of `successor`
+      if loop.isEmpty then
+        continue
+      -- Found a loop, return it
+      return (loop, visited)
+  return (#[], visited.insert node)
+
+/-- Find a loop in the graph and return it. Returns `[]` if there are no loops. -/
+partial def findLoops (arrows : HashMap Name (HashSet Name)) : List Name := Id.run do
+  let mut visited : HashSet Name := {}
+  for node in arrows.toArray.map (·.1) do
+    -- Skip a node if it was already visited
+    if visited.contains node then
+      continue
+    -- `findLoopsAux` returns a loop or `[]` together with a set of nodes it visited on its
+    -- search starting from `node`
+    let (loop, moreVisited) := (findLoopsAux arrows node (visited := visited))
+    visited := moreVisited
+    if !loop.isEmpty then
+      return loop.toList
+  return []
+
 /-- The worlds of a game are joint by dependencies. These are
 automatically computed but can also be defined with the syntax
 `Dependency World₁ → World₂ → World₃`. -/
@@ -837,7 +1120,6 @@ elab "MakeGame" : command => do
              name := item
              displayName := data.displayName
              category := data.category
-              altTitle := data.statement
              hidden := hiddenItems.contains item })


@@ -857,7 +1139,6 @@ elab "MakeGame" : command => do
            displayName := data.displayName
            category := data.category
            locked := false
-            altTitle := data.statement
            hidden := hiddenItems.contains item }
      itemsInWorld := itemsInWorld.insert worldId items

@@ -877,8 +1158,7 @@ elab "MakeGame" : command => do
            displayName := data.displayName
            category := data.category
            locked := false
-            altTitle := data.statement
-            hidden := hiddenItems.contains item }
+            hidden := levelInfo.hidden.contains item }

        -- add the exercise statement from the previous level
        -- if it was named
@@ -891,7 +1171,6 @@ elab "MakeGame" : command => do
              name := name
              displayName := data.displayName
              category := data.category
-              altTitle := data.statement
              locked := false }

        -- add marks for `disabled` and `new` lemmas here, so that they only apply to
@@ -911,16 +1190,18 @@ elab "MakeGame" : command => do
          return level.setComputedInventory inventoryType itemsArray
    allItemsByType := allItemsByType.insert inventoryType allItems

-  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
-    (allItemsByType.findD type {}).toArray.mapM (fun name => do
-      let some item ← getInventoryItem? name type
-        | throwError "Expected item to exist: {name}"
-      return item.toTile)
-  let inventory : InventoryOverview := {
-    lemmas := (← getTiles .Lemma).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
-    tactics := (← getTiles .Tactic).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
-    definitions := (← getTiles .Definition).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
-    lemmaTab := none
-  }
+  saveGameData allItemsByType

-  saveGameData allItemsByType inventory
+/-! # Debugging tools -/
+
+-- /-- Print current game for debugging purposes. -/
+-- elab "PrintCurGame" : command => do
+--   logInfo (toJson (← getCurGame))
+
+/-- Print current level for debugging purposes. -/
+elab "PrintCurLevel" : command => do
+  logInfo (repr (← getCurLevel))
+
+/-- Print levels for debugging purposes. -/
+elab "PrintLevels" : command => do
+  logInfo $ repr $ (← getCurWorld).levels.toArray
@@ -106,8 +106,6 @@ structure InventoryTile where
  new := false
  /-- hide the item in the inventory display -/
  hidden := false
-  /-- hover text -/
-  altTitle : String := default
 deriving ToJson, FromJson, Repr, Inhabited

 def InventoryItem.toTile (item : InventoryItem) : InventoryTile := {
@@ -150,12 +148,6 @@ structure InventoryOverview where
  lemmaTab : Option String
 deriving ToJson, FromJson

-- TODO: Reuse the following code for checking available tactics in user code:
-structure UsedInventory where
-(tactics : HashSet Name := {})
-(definitions : HashSet Name := {})
-(lemmas : HashSet Name := {})
-
 /-! ## Environment extensions for game specification -/

 /-- Register a (non-persistent) environment extension to hold the current level -/
@@ -277,6 +269,13 @@ structure GameLevel where
  image : String := default
 deriving Inhabited, Repr

+structure WorldOverview where
+  world: Name
+  tactics: Array InventoryTile := default
+  definitions: Array InventoryTile := default
+  lemmas: Array InventoryTile := default
+  deriving FromJson, ToJson, Inhabited, Repr
+
 /-- Json-encodable version of `GameLevel`
 Fields:
 - description: Lemma in mathematical language.
@@ -293,7 +292,6 @@ structure LevelInfo where
  descrText : Option String := none
  descrFormat : String := ""
  lemmaTab : Option String
-  module : Name
  displayName : Option String
  statementName : Option String
  template : Option String
@@ -318,7 +316,6 @@ def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo :=
      | some tile => tile.category
      | none => none
    statementName := lvl.statementName.toString
-    module := lvl.module
    displayName := match lvl.statementName with
      | .anonymous => none
      | name => match (inventoryExt.getState env).find?
@@ -383,7 +380,7 @@ structure GameTile where

  TODO: What's the format? -/
  image: String := default
-deriving Inhabited, ToJson, FromJson
+deriving Inhabited, ToJson

 structure Game where
  /-- Internal name of the game. -/
@@ -403,7 +400,7 @@ structure Game where
  tile : GameTile := default
  /-- The path to the background image of the world. -/
  image : String := default
-deriving Inhabited, ToJson, FromJson
+deriving Inhabited, ToJson

 def getGameJson (game : «Game») : Json := Id.run do
  let gameJson : Json := toJson game
@@ -1,8 +1,7 @@
-/- This file is adapted from `Lean/Server/FileWorker.lean`. -/
+/- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/
 import Lean.Server.FileWorker
 import GameServer.Game
 import GameServer.ImportModules
-import GameServer.SaveData

 namespace MyModule
 open Lean
@@ -18,7 +17,7 @@ private def mkEOI (pos : String.Pos) : Syntax :=
  mkNode ``Command.eoi #[atom]

 partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
-  (mps : ModuleParserState) (messages : MessageLog) :
+  (mps : ModuleParserState) (messages : MessageLog) (couldBeEndSnap : Bool) :
    Syntax × ModuleParserState × MessageLog × String.Pos := Id.run do
  let mut pos := mps.pos
  let mut recovering := mps.recovering
@@ -57,20 +56,6 @@ open IO
 open Snapshots
 open JsonRpc

-structure GameWorkerState :=
-  inventory : Array String
-  /--
-  Check for tactics/theorems that are not unlocked.
-  0: no check
-  1: give warnings
-  2: give errors
-  -/
-  difficulty : Nat
-  levelInfo : LevelInfo
-  deriving ToJson, FromJson
-
-abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
-
 section Elab

 def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
@@ -88,30 +73,29 @@ def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : Me
 /-- Find all tactics in syntax object that are forbidden according to a
 set `allowed` of allowed tactics. -/
 partial def findForbiddenTactics (inputCtx : Parser.InputContext)
-    (gameWorkerState : GameWorkerState) (stx : Syntax) :
+    (levelParams : Game.DidOpenLevelParams) (stx : Syntax) :
    Elab.Command.CommandElabM Unit := do
-  let levelInfo := gameWorkerState.levelInfo
  match stx with
  | .missing => return ()
  | .node _info _kind args =>
    for arg in args do
-      findForbiddenTactics inputCtx gameWorkerState arg
+      findForbiddenTactics inputCtx levelParams arg
  | .atom info val =>
    -- ignore syntax elements that do not start with a letter
    -- and ignore "with" keyword
    let allowed := ["with", "fun", "at", "only", "by", "to"]
    if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
      let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-      match levelInfo.tactics.find? (·.name.toString == val) with
+      match levelParams.tactics.find? (·.name.toString == val) with
      | none =>
        -- Note: This case means that the tactic will never be introduced in the game.
-        match gameWorkerState.inventory.find? (· == val) with
+        match levelParams.inventory.find? (· == val) with
        | none =>
          addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
        | some _ => pure () -- tactic is in the inventory, allow it.
      | some tac =>
        if tac.locked then
-          match gameWorkerState.inventory.find? (· == val) with
+          match levelParams.inventory.find? (· == val) with
          | none =>
            addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
          | some _ => pure () -- tactic is in the inventory, allow it.
@@ -125,10 +109,10 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
        let some (.thmInfo ..) := (← getEnv).find? n
          | return () -- not a theorem -> ignore
        -- Forbid the theorem we are proving currently
-        if some n = levelInfo.statementName then
+        if n = levelParams.statementName then
          addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"

-        let lemmasAndDefs := levelInfo.lemmas ++ levelInfo.definitions
+        let lemmasAndDefs := levelParams.lemmas ++ levelParams.definitions
        match lemmasAndDefs.find? (fun l => l.name == n) with
        | none => addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
        | some lem =>
@@ -137,7 +121,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
          else if lem.disabled then
            addWarningMessage info s!"The lemma/definition '{n}' is disabled in this level!"
 where addWarningMessage (info : SourceInfo) (s : MessageData) :=
-  let difficulty := gameWorkerState.difficulty
+  let difficulty := levelParams.difficulty
  if difficulty > 0 then
    modify fun st => { st with
      messages := st.messages.add {
@@ -153,7 +137,7 @@ where addWarningMessage (info : SourceInfo) (s : MessageData) :=

 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
-    (couldBeEndSnap : Bool) (gameWorkerState : GameWorkerState)
+    (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams)
    (initParams : Lsp.InitializeParams) : IO Snapshot := do
  -- Recognize end snap
  if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then
@@ -184,7 +168,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
    Elab.Command.catchExceptions
      (getResetInfoTrees *> do
        let some level ← GameServer.getLevelByFileName? initParams inputCtx.fileName
-          | panic! s!"Level not found: {inputCtx.fileName} / {GameServer.levelIdFromFileName? initParams inputCtx.fileName}"
+          | throwError "Level not found: {inputCtx.fileName}"
        let scope := level.scope

        -- use open namespaces and options as in the level file
@@ -202,12 +186,12 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
            currNamespace := scope.currNamespace,
            openDecls := scope.openDecls }
          let (tacticStx, cmdParserState, msgLog, endOfWhitespace) :=
-            MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog
+            MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog couldBeEndSnap
          modify (fun s => { s with messages := msgLog })
          parseResultRef.set (tacticStx, cmdParserState)

          -- Check for forbidden tactics
-          findForbiddenTactics inputCtx gameWorkerState tacticStx
+          findForbiddenTactics inputCtx levelParams tacticStx

          -- Insert invisible `skip` command to make sure we always display the initial goal
          let skip := Syntax.node (.original default 0 default endOfWhitespace) ``Lean.Parser.Tactic.skip #[]
@@ -235,7 +219,6 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
    }

  let (tacticStx, cmdParserState) ← parseResultRef.get
-  if tacticStx.isMissing then throwServerError "Tactic execution went wrong. No stx found."

  let postCmdSnap : Snapshot := {
    beginPos := tacticStx.getPos?.getD 0
@@ -287,7 +270,7 @@ where

  /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
  private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
-      (gameWorkerState : GameWorkerState) (initParams : Lsp.InitializeParams)
+      (levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams)
      : AsyncElabM (Option Snapshot) := do
    cancelTk.check
    let s ← get
@@ -305,7 +288,7 @@ where
    -- we can see the current goal even on an empty document
    let couldBeEndSnap := s.snaps.size > 1
    let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap
-      gameWorkerState initParams
+      levelParams initParams
    set { s with snaps := s.snaps.push snap }
    -- TODO(MH): check for interrupt with increased precision
    cancelTk.check
@@ -327,7 +310,7 @@ where

  /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
  def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
-      (startAfterMs : UInt32) (gameWorkerState : GameWorkerState)
+      (startAfterMs : UInt32) (levelParams : Game.DidOpenLevelParams)
      : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
    let ctx ← read
    let some headerSnap := snaps[0]? | panic! "empty snapshots"
@@ -343,15 +326,21 @@ where
      publishIleanInfoUpdate m ctx.hOut snaps
      return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
        IO.sleep startAfterMs
-        AsyncList.unfoldAsync (nextSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
+        AsyncList.unfoldAsync (nextSnap ctx m cancelTk levelParams ctx.initParams) { snaps })

 end Elab

+structure GameWorkerState :=
+(levelParams : Game.DidOpenLevelParams)
+
+abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
+
 section Updates

 /-- Given the new document, updates editable doc state. -/
  def updateDocument (newMeta : DocumentMeta) : GameWorkerM Unit := do
    let s ← get
+    let levelParams := s.levelParams
    let ctx ← read
    let oldDoc := (← StateT.lift get).doc
    oldDoc.cancelTk.set
@@ -393,7 +382,7 @@ section Updates
          validSnaps := validSnaps.dropLast
      -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
      -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
-      unfoldSnaps newMeta validSnaps.toArray cancelTk s ctx
+      unfoldSnaps newMeta validSnaps.toArray cancelTk levelParams ctx
        (startAfterMs := ctx.initParams.editDelay.toUInt32)
    StateT.lift <| modify fun st => { st with
      doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
@@ -408,23 +397,24 @@ section Initialization
    fileMap  := default

  def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-      (gameDir : String) (module : Name):
+      (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams) :
      IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
    -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
    let out ← IO.Process.output
-      { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
+      { cwd := levelParams.gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
    if out.exitCode != 0 then
      throwServerError s!"Error while running Lake: {out.stderr}"

    -- Make the paths relative to the current directory
    let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
    let currentDir ← IO.currentDir
-    let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
+    let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p

    -- Set the search path
    Lean.searchPathRef.set paths

-    let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }]
+    let env ← importModules' #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }]
+    -- return (env, paths)

    -- use empty header
    let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
@@ -468,11 +458,10 @@ section Initialization
      return (headerSnap, srcSearchPath)

  def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
-      (gameDir : String) (gameWorkerState : GameWorkerState) : IO (WorkerContext × WorkerState) := do
+       (levelParams : Game.DidOpenLevelParams) : IO (WorkerContext × WorkerState) := do
    let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
-
    let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-      gameDir gameWorkerState.levelInfo.module
+      levelParams initParams
    let cancelTk ← CancelToken.new
    let ctx :=
      { hIn  := i
@@ -483,7 +472,7 @@ section Initialization
        clientHasWidgets
      }
    let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
+      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk levelParams ctx (startAfterMs := 0)
      | Except.error e   => throw (e : ElabTaskError))
    let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
    return (ctx,
@@ -520,7 +509,6 @@ section MessageHandling
    match method with
    | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
    | "$/cancelRequest"        => handle CancelParams (handleCancelRequest ·)
-    | "$/setTrace"        => pure ()
    | "$/lean/rpc/release"     => handle RpcReleaseParams (handleRpcRelease ·)
    | "$/lean/rpc/keepAlive"   => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
    | _                        => throwServerError s!"Got unsupported notification method: {method}"
@@ -559,32 +547,26 @@ section MainLoop
      let doc := st.doc
      doc.cancelTk.set
      return ()
-    | Message.request id "shutdown" none =>
-      ctx.hOut.writeLspResponse ⟨id, Json.null⟩
+    | Message.notification "$/game/setInventory" params =>
+      let p := (← parseParams Game.SetInventoryParams (toJson params))
+      let s ← get
+
+      set {s with levelParams := {s.levelParams with
+        inventory := p.inventory,
+        difficulty := p.difficulty}}
      mainLoop
    | Message.notification method (some params) =>
      handleNotification method (toJson params)
      mainLoop
-    | _ => throwServerError s!"Got invalid JSON-RPC message: {toJson msg}"
+    | _ => throwServerError "Got invalid JSON-RPC message"
 end MainLoop

-def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do
+def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
  let i ← maybeTee "fwIn.txt" false i
  let o ← maybeTee "fwOut.txt" true o
-  let initRequest ← i.readLspRequestAs "initialize" Game.InitializeParams
-  o.writeLspResponse {
-    id     := initRequest.id
-    result := {
-      capabilities := Watchdog.mkLeanServerCapabilities
-      serverInfo?  := some {
-        name     := "Lean 4 Game Server"
-        version? := "0.1.1"
-      }
-      : InitializeResult
-    }
-  }
-  discard $ i.readLspNotificationAs "initialized" InitializedParams
+  let initParams ← i.readLspRequestAs "initialize" InitializeParams
  let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
+  let ⟨_, levelParams⟩ ← i.readLspNotificationAs "$/game/didOpenLevel" Game.DidOpenLevelParams

  let doc := param.textDocument
  /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
@@ -596,24 +578,9 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
  let e := e.withPrefix s!"[{param.textDocument.uri}] "
  let _ ← IO.setStderr e
  try
-    let game ← loadGameData gameDir
-    -- TODO: We misuse the `rootUri` field to the gameName
-    let rootUri? : Option String := some (toString game.name)
-    let initParams := {initRequest.param.toLeanInternal with rootUri?}
-    let some (levelId : LevelId) := GameServer.levelIdFromFileName?
-        initParams meta.mkInputContext.fileName
-      | throwServerError s!"Could not determine level ID: {meta.mkInputContext.fileName}"
-    let levelInfo ← loadLevelData gameDir levelId.world levelId.level
-    let some initializationOptions := initRequest.param.initializationOptions?
-      | throwServerError "no initialization options found"
-    let gameWorkerState : GameWorkerState:= {
-      inventory := initializationOptions.inventory
-      difficulty := initializationOptions.difficulty
-      levelInfo
-    }
-    let (ctx, st) ← initializeWorker meta i o e initParams opts gameDir gameWorkerState
+    let (ctx, st) ← initializeWorker meta i o e initParams.param opts levelParams
    let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
-      StateT.run (s := gameWorkerState) <| (mainLoop)
+      StateT.run (s := {levelParams := levelParams}) <| (mainLoop)
    return (0 : UInt32)
  catch e =>
    IO.eprintln e
@@ -623,13 +590,12 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
      message := e.toString }] o
    return (1 : UInt32)

-def workerMain (opts : Options) (args : List String): IO UInt32 := do
+def workerMain (opts : Options) : IO UInt32 := do
  let i ← IO.getStdin
  let o ← IO.getStdout
  let e ← IO.getStderr
  try
-    let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
-    let exitCode ← initAndRunWorker i o e opts gameDir
+    let exitCode ← initAndRunWorker i o e opts
    -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't
    -- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code
    o.flush
@@ -25,56 +25,123 @@ open Lsp
 open JsonRpc
 open IO

-/- Game-specific version of `InitializeParams` that allows for extra options: -/
-
-structure InitializationOptions extends Lean.Lsp.InitializationOptions :=
-  difficulty : Nat
+structure DidOpenLevelParams where
+  uri : String
+  gameDir : String
+  levelModule : Name
+  tactics : Array InventoryTile
+  lemmas : Array InventoryTile
+  definitions : Array InventoryTile
  inventory : Array String
+  /--
+  Check for tactics/theorems that are not unlocked.
+  0: no check
+  1: give warnings
+  2: give errors
+  -/
+  difficulty : Nat
+  /-- The name of the theorem to be proven in this level. -/
+  statementName : Name
  deriving ToJson, FromJson

-structure InitializeParams where
-  processId? : Option Int := none
-  clientInfo? : Option ClientInfo := none
-  /- We don't support the deprecated rootPath
-  (rootPath? : Option String) -/
-  rootUri? : Option String := none
-  initializationOptions? : Option InitializationOptions := none
-  capabilities : ClientCapabilities
-  /-- If omitted, we default to off. -/
-  trace : Trace := Trace.off
-  workspaceFolders? : Option (Array WorkspaceFolder) := none
-  deriving ToJson
+structure SetInventoryParams where
+  inventory : Array String
+  difficulty : Nat
+deriving ToJson, FromJson

-instance : FromJson InitializeParams where
-  fromJson? j := do
-    let processId? := j.getObjValAs? Int "processId"
-    let clientInfo? := j.getObjValAs? ClientInfo "clientInfo"
-    let rootUri? := j.getObjValAs? String "rootUri"
-    let initializationOptions? := j.getObjValAs? InitializationOptions "initializationOptions"
-    let capabilities ← j.getObjValAs? ClientCapabilities "capabilities"
-    let trace := (j.getObjValAs? Trace "trace").toOption.getD Trace.off
-    let workspaceFolders? := j.getObjValAs? (Array WorkspaceFolder) "workspaceFolders"
-    return ⟨
-      processId?.toOption,
-      clientInfo?.toOption,
-      rootUri?.toOption,
-      initializationOptions?.toOption,
-      capabilities,
-      trace,
-      workspaceFolders?.toOption⟩
-
-def InitializeParams.toLeanInternal (p : InitializeParams) : Lean.Lsp.InitializeParams :=
-{
-  processId? := p.processId?
-  clientInfo? := p.clientInfo?
-  rootUri? := p.rootUri?
-  initializationOptions? := p.initializationOptions?.map fun o => {
-    editDelay? := o.editDelay?
-    hasWidgets? := o.hasWidgets?
+def handleDidOpenLevel (params : Json) : GameServerM Unit := do
+  let p ← parseParams _ params
+  let m := p.textDocument
+  -- Execute the regular handling of the `didOpen` event
+  handleDidOpen p
+  let fw ← findFileWorker! m.uri
+  -- let s ← get
+  let c ← read
+  let some lvl ← GameServer.getLevelByFileName? c.initParams ((System.Uri.fileUriToPath? m.uri).getD m.uri |>.toString)
+    | do
+      c.hLog.putStr s!"Level not found: {m.uri} {c.initParams.rootUri?}"
+      c.hLog.flush
+  -- Send an extra notification to the file worker to inform it about the level data
+  let s ← get
+  fw.stdin.writeLspNotification {
+    method := "$/game/didOpenLevel"
+    param  := {
+      uri := m.uri
+      gameDir := s.gameDir
+      levelModule := lvl.module
+      tactics := lvl.tactics.tiles
+      lemmas := lvl.lemmas.tiles
+      definitions := lvl.definitions.tiles
+      inventory := s.inventory
+      difficulty := s.difficulty
+      statementName := lvl.statementName
+      : DidOpenLevelParams
+    }
  }
-  capabilities := p.capabilities
-  trace := p.trace
-  workspaceFolders? := p.workspaceFolders?
-}
+
+partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
+  match ev with
+  | ServerEvent.clientMsg msg =>
+    match msg with
+    | Message.notification "$/game/setInventory" params =>
+      let p := (← parseParams SetInventoryParams (toJson params))
+      let s ← get
+      set {s with inventory := p.inventory, difficulty := p.difficulty}
+      let st ← read
+      let workers ← st.fileWorkersRef.get
+      for (_, fw) in workers do
+        fw.stdin.writeLspMessage msg
+
+      return true
+    | Message.request id "loadInventoryOverview" _ =>
+      let s ← get
+      let some game ← getGame? s.game
+        | return false
+
+      let mut overview : Array WorldOverview := #[]
+      for ⟨worldId, world⟩ in game.worlds.nodes.toList do
+        let mut tactics : Array InventoryTile := #[]
+        let mut theorems : Array InventoryTile := #[]
+        let mut definitions : Array InventoryTile := #[]
+        for ⟨_levelId, lvl⟩ in world.levels.toList do
+          tactics := tactics ++ lvl.tactics.tiles.filterMap (fun tile => match tile.new with
+            | true => some {tile with new := false, locked := true, disabled := false}
+            | false => none)
+          theorems := theorems ++ lvl.lemmas.tiles.filterMap (fun tile => match tile.new with
+            | true => some {tile with new := false, locked := true, disabled := false}
+            | false => none)
+          definitions := definitions ++ lvl.definitions.tiles.filterMap (fun tile => match tile.new with
+            | true => some {tile with new := false, locked := true, disabled := false}
+            | false => none)
+        overview := overview.push {
+          world := worldId,
+          tactics := tactics,
+          lemmas := theorems,
+          definitions := definitions }
+      let c ← read
+      c.hOut.writeLspResponse ⟨id, ToJson.toJson overview⟩
+      return true
+      -- -- All Levels have the same tiles, so we just load them from level 1 of an arbitrary world
+      -- -- and reset `new`, `disabled` and `unlocked`.
+      -- -- Note: as we allow worlds without any levels (for developing), we might need
+      -- -- to try until we find the first world with levels.
+      -- for ⟨worldId, _⟩ in game.worlds.nodes.toList do
+      --   let some lvl ← getLevel? {game := s.game, world := worldId, level := 1}
+      --     | do continue
+      --   let inventory : InventoryOverview := {
+      --     tactics := lvl.tactics.tiles.map
+      --       ({ · with locked := true, disabled := false, new := false }),
+      --     lemmas := lvl.lemmas.tiles.map
+      --       ({ · with locked := true, disabled := false, new := false }),
+      --     definitions := lvl.definitions.tiles.map
+      --       ({ · with locked := true, disabled := false, new := false }),
+      --     lemmaTab := none
+      --   }
+      --   let c ← read
+      --   c.hOut.writeLspResponse ⟨id, ToJson.toJson inventory⟩
+      --   return true
+      -- return false
+    | _ => return false
+  | _ => return false

 end Game
@@ -18,14 +18,6 @@ instance [ToJson β] : ToJson (Graph Name β) := {
  ]
 }

-- Just a dummy implementation for now:
-instance : FromJson (Graph Name β) := {
-  fromJson? := fun _ => .ok {
-    nodes := {}
-    edges := {}
-  }
-}
-
 instance  : EmptyCollection (Graph α β) := ⟨default⟩

 def Graph.insertNode (g : Graph α β) (a : α) (b : β) :=
@@ -1,190 +0,0 @@
-import Lean
-
-/-! This document contains various things which cluttered `Commands.lean`. -/
-
-open Lean Meta Elab Command
-
-syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
-
-/-! ## Doc Comment Parsing -/
-
-/-- Read a doc comment and get its content. Return `""` if no doc comment available. -/
-def parseDocComment! (doc: Option (TSyntax `Lean.Parser.Command.docComment)) :
-    CommandElabM String := do
-  match doc with
-  | none =>
-    logWarning "Add a text to this command with `/-- yada yada -/ MyCommand`!"
-    pure ""
-  | some s => match s.raw[1] with
-    | .atom _ val => pure <| val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩))
-    | _           => pure "" --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}"
-
-/-- Read a doc comment and get its content. Return `none` if no doc comment available. -/
-def parseDocComment (doc: Option (TSyntax `Lean.Parser.Command.docComment)) :
-    CommandElabM <| Option String := do
-  match doc with
-  | none => pure none
-  | some _ => parseDocComment! doc
-
-
-/-- TODO: This is only used to provide some backwards compatibility and you can
-replace `parseDocCommentLegacy` with `parseDocComment` in the future. -/
-def parseDocCommentLegacy (doc: Option (TSyntax `Lean.Parser.Command.docComment))
-    (t : Option (TSyntax `str)) : CommandElabM <| String := do
-  match doc with
-  | none =>
-    match t with
-    | none =>
-      pure <| ← parseDocComment! doc
-    | some t =>
-      logWarningAt t "You should use the new Syntax:
-
-      /-- yada yada -/
-      YourCommand
-
-      instead of
-
-      YourCommand \"yada yada\"
-      "
-      pure t.getString
-  | some _ =>
-    match t with
-      | none =>
-        pure <| ← parseDocComment! doc
-      | some t =>
-        logErrorAt t "You must not provide both, a docstring and a string following the command!
-        Only use
-
-        /-- yada yada -/
-        YourCommand
-
-        and remove the string following it!"
-        pure <| ← parseDocComment! doc
-
-/-! ## Statement string -/
-
-def getStatement (name : Name) : CommandElabM MessageData := do
-  return ← addMessageContextPartial (.ofPPFormat { pp := fun
-    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
-    | none     => return "that's a bug." })
-
-- Note: We use `String` because we can't send `MessageData` as json, but
-- `MessageData` might be better for interactive highlighting.
-/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`.
-
-Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
-`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
-def getStatementString (name : Name) : CommandElabM String := do
-  try
-    return ← (← getStatement name).toString
-  catch
-  | _ => throwError m!"Could not find {name} in context."
-  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.
-
-/-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
-syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
-- TODO
-
-
-/-- Remove any spaces at the beginning of a new line -/
-partial def removeIndentation (s : String) : String :=
-  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
-    let c := s.get i
-    let i := s.next i
-    if s.atEnd i then
-      acc.push c
-    else if removeSpaces && c == ' ' then
-      loop i acc (removeSpaces := true)
-    else if c == '\n' then
-      loop i (acc.push c) (removeSpaces := true)
-    else
-      loop i (acc.push c)
-  loop ⟨0⟩ ""
-
-
-/-! ## Loops in Graph-like construct
-
-TODO: Why are we not using graphs here but our own construct `HashMap Name (HashSet Name)`?
-/
-
-partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name))
-      (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) :
-    HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do
-  match (newArrows.find? id, decendants.find? id) with
-  | (some _, some _) => return (newArrows, decendants)
-  | _ =>
-    let mut newArr := newArrows
-    let mut desc := decendants
-    desc := desc.insert id {} -- mark as worked in case of loops
-    newArr := newArr.insert id {} -- mark as worked in case of loops
-    let children := arrows.findD id {}
-    let mut trimmedChildren := children
-    let mut theseDescs := children
-    for child in children do
-      (newArr, desc) := removeTransitiveAux child arrows newArr desc
-      let childDescs := desc.findD child {}
-      theseDescs := theseDescs.insertMany childDescs
-      for d in childDescs do
-        trimmedChildren := trimmedChildren.erase d
-    desc := desc.insert id theseDescs
-    newArr := newArr.insert id trimmedChildren
-    return (newArr, desc)
-
-
-def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do
-  let mut newArr := {}
-  let mut desc := {}
-  for id in arrows.toArray.map Prod.fst do
-    (newArr, desc) := removeTransitiveAux id arrows newArr desc
-    if (desc.findD id {}).contains id then
-      logError <| m!"Loop at {id}. " ++
-        m!"This should not happen and probably means that `findLoops` has a bug."
-      -- DEBUG:
-      -- for ⟨x, hx⟩ in desc.toList do
-      --   m := m ++ m!"{x}: {hx.toList}\n"
-      -- logError m
-
-  return newArr
-
-/-- The recursive part of `findLoops`. Finds loops that appear as successors of `node`.
-
-For performance reason it returns a HashSet of visited
-nodes as well. This is filled with all nodes ever looked at as they cannot be
-part of a loop anymore. -/
-partial def findLoopsAux (arrows : HashMap Name (HashSet Name)) (node : Name)
-    (path : Array Name := #[]) (visited : HashSet Name := {}) :
-    Array Name × HashSet Name := Id.run do
-  let mut visited := visited
-  match path.getIdx? node with
-  | some i =>
-    -- Found a loop: `node` is already the iᵗʰ element of the path
-    return (path.extract i path.size, visited.insert node)
-  | none =>
-    for successor in arrows.findD node {} do
-      -- If we already visited the successor, it cannot be part of a loop anymore
-      if visited.contains successor then
-        continue
-      -- Find any loop involving `successor`
-      let (loop, _) := findLoopsAux arrows successor (path.push node) visited
-      visited := visited.insert successor
-      -- No loop found in the dependants of `successor`
-      if loop.isEmpty then
-        continue
-      -- Found a loop, return it
-      return (loop, visited)
-  return (#[], visited.insert node)
-
-/-- Find a loop in the graph and return it. Returns `[]` if there are no loops. -/
-partial def findLoops (arrows : HashMap Name (HashSet Name)) : List Name := Id.run do
-  let mut visited : HashSet Name := {}
-  for node in arrows.toArray.map (·.1) do
-    -- Skip a node if it was already visited
-    if visited.contains node then
-      continue
-    -- `findLoopsAux` returns a loop or `[]` together with a set of nodes it visited on its
-    -- search starting from `node`
-    let (loop, moreVisited) := (findLoopsAux arrows node (visited := visited))
-    visited := moreVisited
-    if !loop.isEmpty then
-      return loop.toList
-  return []
@@ -1,152 +0,0 @@
-import Lean
-import GameServer.EnvExtensions
-
-open Lean Elab Command
-
-/-- Copied from `Mathlib.Tactic.HelpCmd`.
-
-Gets the initial string token in a parser description. For example, for a declaration like
-`syntax "bla" "baz" term : tactic`, it returns `some "bla"`. Returns `none` for syntax declarations
-that don't start with a string constant. -/
-partial def getHeadTk (e : Expr) : Option String :=
-  match (Expr.withApp e λ e a => (e.constName?.getD Name.anonymous, a)) with
-  | (``ParserDescr.node, #[_, _, p]) => getHeadTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getHeadTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getHeadTk p
-  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getHeadTk p
-  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
-  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => some tk
-  | (``Parser.withAntiquot, #[_, p]) => getHeadTk p
-  | (``Parser.leadingNode, #[_, _, p]) => getHeadTk p
-  | (``HAndThen.hAndThen, #[_, _, _, _, p, _]) => getHeadTk p
-  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
-  | (``Parser.symbol, #[.lit (.strVal tk)]) => some tk
-  | _ => none
-
-/-! ## Doc entries -/
-
-/-- Modified from `#help` in `Mathlib.Tactic.HelpCmd` -/
-def getTacticDocstring (env : Environment) (name: Name) : CommandElabM (Option String) := do
-  let name := name.toString (escape := false)
-  let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {}
-
-  let catName : Name := `tactic
-  let catStx : Ident := mkIdent catName -- TODO
-  let some cat := (Parser.parserExtension.getState env).categories.find? catName
-    | throwErrorAt catStx "{catStx} is not a syntax category"
-  liftTermElabM <| Term.addCategoryInfo catStx catName
-  for (k, _) in cat.kinds do
-    let mut used := false
-    if let some tk := do getHeadTk (← (← env.find? k).value?) then
-      let tk := tk.trim
-      if name ≠ tk then -- was `!name.isPrefixOf tk`
-        continue
-      used := true
-      decls := decls.insert tk ((decls.findD tk #[]).push k)
-  for (_name, ks) in decls do
-    for k in ks do
-      if let some doc ← findDocString? env k then
-        return doc
-
-  logWarning <| m!"Could not find a docstring for tactic {name}, consider adding one " ++
-    m!"using `TacticDoc {name} \"some doc\"`"
-  return none
-
-/-- Retrieve the docstring associated to an inventory item. For Tactics, this
-is not guaranteed to work. -/
-def getDocstring (env : Environment) (name : Name) (type : InventoryType) :
-    CommandElabM (Option String) :=
-  match type with
-  -- for tactics it's a lookup following mathlib's `#help`. not guaranteed to be the correct one.
-  | .Tactic => getTacticDocstring env name
-  | .Lemma => findDocString? env name
-  -- TODO: for definitions not implemented yet, does it work?
-  | .Definition => findDocString? env name
-
-/-- Checks if `inventoryTemplateExt` contains an entry with `(type, name)` and yields
-a warning otherwise. If `template` is provided, it will add such an entry instead of yielding a
-warning.
-
-`ref` is the syntax piece. If `name` is not provided, it will use `ident.getId`.
-I used this workaround, because I needed a new name (with correct namespace etc)
-to be used, and I don't know how to create a new ident with same position but different name.
-/
-def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.getId)
-    (template : Option String := none) : CommandElabM Unit := do
-  -- note: `name` is an `Ident` (instead of `Name`) for the log messages.
-  let env ← getEnv
-  let n := name
-  -- Find a key with matching `(type, name)`.
-  match (inventoryTemplateExt.getState env).findIdx?
-    (fun x => x.name == n && x.type == type) with
-  -- Nothing to do if the entry exists
-  | some _ => pure ()
-  | none =>
-    match template with
-    -- Warn about missing documentation
-    | none =>
-      let docstring ← match (← getDocstring env name type) with
-      | some ds =>
-        logInfoAt ref (m!"Missing {type} Documentation. Using existing docstring. " ++
-        m!"Add {name}\nAdd `{type}Doc {name}` somewhere above this statement.")
-        pure s!"*(lean docstring)*\\\n{ds}"
-      | none =>
-        logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
-        m!"somewhere above this statement.")
-        pure "(missing)"
-
-      -- We just add a dummy entry
-      modifyEnv (inventoryTemplateExt.addEntry · {
-        type := type
-        name := name
-        category := if type == .Lemma then s!"{n.getPrefix}" else ""
-        content := docstring})
-    -- Add the default documentation
-    | some s =>
-      modifyEnv (inventoryTemplateExt.addEntry · {
-        type := type
-        name := name
-        category := if type == .Lemma then s!"{n.getPrefix}" else ""
-        content := s })
-      logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++
-        m!"docstring) instead. If you want to write a different description, add " ++
-        m!"`{type}Doc {name}` somewhere above this statement.")
-
-partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : CommandElabM UsedInventory := do
-  match stx with
-  | .missing => return acc
-  | .node _info kind args =>
-    if kind == `GameServer.Tactic.Hint || kind == `GameServer.Tactic.Branch then return acc
-    return ← args.foldlM (fun acc arg => collectUsedInventory arg acc) acc
-  | .atom _info val =>
-    -- ignore syntax elements that do not start with a letter
-    -- and ignore some standard keywords
-    let allowed := ["with", "fun", "at", "only", "by"]
-    if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
-      let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-      return {acc with tactics := acc.tactics.insert val}
-    else
-      return acc
-  | .ident _info _rawVal val _preresolved =>
-      let ns ←
-        try resolveGlobalConst (mkIdent val)
-        catch | _ => pure [] -- catch "unknown constant" error
-      return ← ns.foldlM (fun acc n => do
-        if let some (.thmInfo ..) := (← getEnv).find? n then
-          return {acc with lemmas := acc.lemmas.insertMany ns}
-        else
-          return {acc with definitions := acc.definitions.insertMany ns}
-      ) acc
-
-- #check expandOptDocComment?
-
-def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
-| .Tactic => level.tactics
-| .Definition => level.definitions
-| .Lemma => level.lemmas
-
-def GameLevel.setComputedInventory (level : GameLevel) :
-    InventoryType → Array InventoryTile → GameLevel
-| .Tactic, v =>     {level with tactics     := {level.tactics     with tiles := v}}
-| .Definition, v => {level with definitions := {level.definitions with tiles := v}}
-| .Lemma, v =>      {level with lemmas      := {level.lemmas      with tiles := v}}
@@ -1,17 +0,0 @@
-import Lean
-
-/-! This document contains custom options available in the game. -/
-
-/-- Let `MakeGame` print the reasons why the worlds depend on each other. -/
-register_option lean4game.showDependencyReasons : Bool := {
-  defValue := false
-  descr := "show reasons for calculated world dependencies."
-}
-
-/-- Let `MakeGame` print the reasons why the worlds depend on each other.
-
-Note: currently unused in favour of setting `set_option trace.debug true`. -/
-register_option lean4game.verbose : Bool := {
-  defValue := false
-  descr := "display more info messages to help developing the game."
-}
@@ -46,8 +46,8 @@ partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) :
  | .bvar i1, .bvar i2 => if i1 == i2 then bij else none
  | .fvar i1, .fvar i2 => bij.insert? i1 i2
  | .mvar _, .mvar _ => bij
-  | .sort _u1, .sort _u2 => bij -- TODO?
-  | .const n1 _ls1, .const n2 _ls2 =>
+  | .sort u1, .sort u2 => bij -- TODO?
+  | .const n1 ls1, .const n2 ls2 =>
    if n1 == n2 then bij else none -- && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2)
  | .app f1 a1, .app f2 a2 =>
    some bij
@@ -1,78 +0,0 @@
-import GameServer.EnvExtensions
-
-open Lean Meta Elab Command
-
-
-/-! ## Copy images -/
-
-open IO.FS System FilePath in
-/-- Copies the folder `images/` to `.lake/gamedata/images/` -/
-def copyImages : IO Unit := do
-  let target : FilePath := ".lake" / "gamedata"
-  if ← FilePath.pathExists "images" then
-    for file in ← walkDir "images" do
-      let outFile := target.join file
-      -- create the directories
-      if ← file.isDir then
-        createDirAll outFile
-      else
-        if let some parent := outFile.parent then
-          createDirAll parent
-        -- copy file
-        let content ← readBinFile file
-        writeBinFile outFile content
-
-namespace GameData
-  def gameDataPath : System.FilePath := ".lake" / "gamedata"
-  def gameFileName := s!"game.json"
-  def docFileName := fun (inventoryType : InventoryType) (name : Name) => s!"doc__{inventoryType}__{name}.json"
-  def levelFileName := fun (worldId : Name) (levelId : Nat) => s!"level__{worldId}__{levelId}.json"
-  def inventoryFileName := s!"inventory.json"
-end GameData
-
-open GameData in
-- TODO: register all of this as ToJson instance?
-def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
-    (inventory : InventoryOverview): CommandElabM Unit := do
-  let game ← getCurGame
-  let env ← getEnv
-  let path := (← IO.currentDir) / gameDataPath
-
-  if ← path.isDir then
-    IO.FS.removeDirAll path
-  IO.FS.createDirAll path
-
-  -- copy the images folder
-  copyImages
-
-  for (worldId, world) in game.worlds.nodes.toArray do
-    for (levelId, level) in world.levels.toArray do
-      IO.FS.writeFile (path / levelFileName worldId levelId) (toString (toJson (level.toInfo env)))
-
-  IO.FS.writeFile (path / gameFileName) (toString (getGameJson game))
-
-  for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
-    for name in allItemsByType.findD inventoryType {} do
-      let some item ← getInventoryItem? name inventoryType
-        | throwError "Expected item to exist: {name}"
-      IO.FS.writeFile (path / docFileName inventoryType name) (toString (toJson item))
-
-  IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))
-
-open GameData
-
-def loadData (f : System.FilePath) (α : Type) [FromJson α] : IO α := do
-  let str ← IO.FS.readFile f
-  let json ← match Json.parse str with
-  | .ok v => pure v
-  | .error e => throw (IO.userError e)
-  let data ← match fromJson? json with
-  | .ok v => pure v
-  | .error e => throw (IO.userError e)
-  return data
-
-def loadGameData (gameDir : System.FilePath) : IO Game :=
-  loadData (gameDir / gameDataPath / gameFileName) Game
-
-def loadLevelData (gameDir : System.FilePath) (worldId : Name) (levelId : Nat) : IO LevelInfo :=
-  loadData (gameDir / gameDataPath / levelFileName worldId levelId) LevelInfo
@@ -0,0 +1,158 @@
+/- This file is mostly copied from `Lean/Server/Watchdog.lean`. -/
+import Lean.Server.Watchdog
+import GameServer.Game
+
+namespace MyServer.Watchdog
+open Lean
+open Server
+open Watchdog
+open IO
+open Lsp
+open JsonRpc
+open System.Uri
+
+  partial def mainLoop (clientTask : Task ServerEvent) : GameServerM Unit := do
+    let st ← read
+    let workers ← st.fileWorkersRef.get
+    let mut workerTasks := #[]
+    for (_, fw) in workers do
+      if let WorkerState.running := fw.state then
+        workerTasks := workerTasks.push <| fw.commTask.map (ServerEvent.workerEvent fw)
+
+    let ev ← IO.waitAny (clientTask :: workerTasks.toList)
+
+    if ← Game.handleServerEvent ev then -- handle Game requests
+      mainLoop (←runClientTask)
+    else
+      match ev with
+      | ServerEvent.clientMsg msg =>
+        match msg with
+        | Message.request id "shutdown" _ =>
+          shutdown
+          st.hOut.writeLspResponse ⟨id, Json.null⟩
+        | Message.request id method (some params) =>
+          handleRequest id method (toJson params)
+          mainLoop (←runClientTask)
+        | Message.response .. =>
+          -- TODO: handle client responses
+          mainLoop (←runClientTask)
+        | Message.responseError _ _ e .. =>
+          throwServerError s!"Unhandled response error: {e}"
+        | Message.notification method (some params) =>
+          if method == "textDocument/didOpen" then
+            -- for lean4game, we need to pass in extra information when a level is opened:
+            Game.handleDidOpenLevel (← parseParams _ (toJson params))
+          else
+            handleNotification method (toJson params)
+          mainLoop (←runClientTask)
+        | _ => throwServerError "Got invalid JSON-RPC message"
+      | ServerEvent.clientError e => throw e
+      | ServerEvent.workerEvent fw ev =>
+        match ev with
+        | WorkerEvent.ioError e =>
+          throwServerError s!"IO error while processing events for {fw.doc.uri}: {e}"
+        | WorkerEvent.crashed _ =>
+          handleCrash fw.doc.uri #[]
+          mainLoop clientTask
+        | WorkerEvent.terminated =>
+          throwServerError "Internal server error: got termination event for worker that should have been removed"
+        | .importsChanged =>
+          startFileWorker fw.doc
+          mainLoop clientTask
+
+def initAndRunWatchdogAux : GameServerM Unit := do
+  let st ← read
+  try
+    discard $ st.hIn.readLspNotificationAs "initialized" InitializedParams
+    let clientTask ← runClientTask
+    mainLoop clientTask
+  catch err =>
+    shutdown
+    throw err
+  /- NOTE(WN): It looks like instead of sending the `exit` notification,
+  VSCode just closes the stream. In that case, pretend we got an `exit`. -/
+  let Message.notification "exit" none ←
+    try st.hIn.readLspMessage
+    catch _ => pure (Message.notification "exit" none)
+    | throwServerError "Got `shutdown` request, expected an `exit` notification"
+
+def createEnv (gameDir : String) (module : String) : IO Environment := do
+  -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
+  let out ← IO.Process.output
+    { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
+  if out.exitCode != 0 then
+    throwServerError s!"Error while running Lake: {out.stderr}"
+
+  -- Make the paths relative to the current directory
+  let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
+  let currentDir ← IO.currentDir
+  let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
+
+  -- Set the search path
+  Lean.searchPathRef.set paths
+
+  let env ← importModules #[{ module := `Init : Import }, { module := module : Import }] {} 0
+  return env
+
+def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
+  if args.length < 2 then
+    throwServerError s!"Expected 1-3 command line arguments in addition to `--server`:
+      game directory, the name of the main module (optional), and the name of the game (optional)."
+  let gameDir := args[1]!
+  let module := if args.length < 3 then defaultGameModule else args[2]!
+  let gameName := if args.length < 4 then defaultGameName else args[3]!
+  let workerPath := "./gameserver"
+  -- TODO: Do the following commands slow us down?
+  let srcSearchPath ← initSrcSearchPath (← getBuildDir)
+  let references ← IO.mkRef (← loadReferences)
+  let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
+  let i ← maybeTee "wdIn.txt" false i
+  let o ← maybeTee "wdOut.txt" true o
+  let e ← maybeTee "wdErr.txt" true e
+  let state := {
+    env := ← createEnv gameDir module,
+    game := gameName,
+    gameDir := gameDir,
+    inventory := #[]
+    difficulty := 0
+    }
+  let initRequest ← i.readLspRequestAs "initialize" InitializeParams
+  -- We misuse the `rootUri` field to the gameName
+  let rootUri? := gameName
+  let initRequest := {initRequest with param := {initRequest.param with rootUri?}}
+  o.writeLspResponse {
+    id     := initRequest.id
+    result := {
+      capabilities := mkLeanServerCapabilities
+      serverInfo?  := some {
+        name     := "Lean 4 Game Server"
+        version? := "0.1.1"
+      }
+      : InitializeResult
+    }
+  }
+  let context : ServerContext := {
+    hIn            := i
+    hOut           := o
+    hLog           := e
+    args           := args
+    fileWorkersRef := fileWorkersRef
+    initParams     := initRequest.param
+    workerPath
+    srcSearchPath
+    references
+  }
+  discard $ ReaderT.run (StateT.run initAndRunWatchdogAux state) context
+
+def watchdogMain (args : List String) : IO UInt32 := do
+  let i ← IO.getStdin
+  let o ← IO.getStdout
+  let e ← IO.getStderr
+  try
+    initAndRunWatchdog args i o e
+    return 0
+  catch err =>
+    e.putStrLn s!"Watchdog error: {err}"
+    return 1
+
+end MyServer.Watchdog
@@ -1,4 +1,5 @@
 import GameServer.FileWorker
+import GameServer.Watchdog
 import GameServer.Commands

 -- TODO: The only reason we import `Commands` is so that it gets built to on `lake build`
@@ -9,9 +10,13 @@ unsafe def main : List String → IO UInt32 := fun args => do

  Lean.enableInitializersExecution

-  -- TODO: remove this argument
  if args[0]? == some "--server" then
-    MyServer.FileWorker.workerMain {} args
+    MyServer.Watchdog.watchdogMain args
+  else if args[0]? == some "--worker" then
+    MyServer.FileWorker.workerMain {}
  else
-    e.putStrLn s!"Expected `--server`"
+    e.putStrLn s!"Expected `--server` or `--worker`"
    return 1
+
+
+-- TODO: Potentially it could be useful to pass in the `gameName` via the websocket connection
@@ -12,7 +12,7 @@ lean_lib GameServer

@[default_target]
 lean_exe gameserver {
-  root := `GameServer
+  root := `Main
  supportInterpreter := true
 }
Author	SHA1	Message	Date
Jon Eugster	bb214f426b	Merge branch 'dev' into world_overviews	2023-12-10 00:18:47 +01:00
joneugster	4266c090db	WIP progress on world overviews	2023-10-23 15:41:29 +02:00