work on network interruption errors

Fix typos

.github/workflows/build.yml

@@ -3,7 +3,7 @@ run-name: Build the project
 on: [push]
 jobs:
   build:
-    runs-on: ubuntu-20.04
+    runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
       - uses: actions/setup-node@v3

README.md

@@ -1,33 +1,36 @@
 # Lean 4 Game
 
-This is a prototype for a Lean 4 game platform. The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
+This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
+
+The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
 (NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
 of Kevin Buzzard and Mohammad Pedramfar.
 The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
 
-### Progress & Contributing
-Currently the interface is still undergoing bigger changes, contributions are of course welcome, but it might be better to wait with them for a bit until proper support for external games is implemented and the existing games are separated from this repository. (ca. Sept. 2023)
+## Creating a Game
 
+Please follow the tutorial [Creating a Game](doc/create_game.md).
+In particular step 5 thereof explains [How to Run Games Locally](doc/running_locally.md).
 
-### Documentation
+### Publishing a Game
 
-For game developers, there is a work-in-progress Documentation: [Create a Game](DOCUMENTATION.md).
-Best to talk with us directly.
+We encourage anybody to have games hosted on our [Lean Game Server](https://adam.math.hhu.de) for anybody to play. For that you simply need to contact us with the link to your game repo. We are also happy to add work-in-progress games and games in any language.
 
-For the game engine itself, documentation is missing currently.
+For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).
 
-## NPM Scripts
+## Documentation
 
-* `npm start`: Start the project in development mode. The browser will automatically reload when client files get changed. The Lean server will get recompiled and restarted when lean files get changed. The Lean server will be started without a container. The client and server can be started separately using the scripts `npm run start_client` and `npm run start_server`. The project can be accessed via `http://localhost:3000`.
-Internally, websocket requests to `ws://localhost:3000/websockets` will be forwarded to a Lean server running on port `8080`.
+The documentation for the game engine itself is still missing, but there is [Creating a Game](doc/create_game.md) explaining the API to create a game.
 
-* `npm run build`: Build the project in production mode. All assets of the client will be compiled into `client/dist`.
-On the server side, the command will set up a docker image containing the Lean server. The two parts can be built separately using `npm run build_client` and `npm run build_server`.
+Some documentation:
 
-* `npm run production`: Start the project in production mode. This requires that the build script has been run. It will start a server on the port specified in the `PORT` environment variable or by default on `8080`. You can run on a specifiv port by running `PORT=80 npm run production`. The server will serve the files in `client/dist` via http and give access to the docker-contained Lean server via the web socket protocol.
+- [NPM Scripts](doc/npm_scripts.md)
+- [Old documentation](doc/DOCUMENTATION.md)
 
+## Contributing
+
+Contributions to `lean4game` are always welcome!
 
 ## Security
 
-Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server in a Docker container
-secured by [gVisor](https://gvisor.dev/).
+Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server with bubblewrap.

client/src/app.tsx

@@ -6,33 +6,23 @@ import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
 
-import './reset.css';
-import './app.css';
+import './css/reset.css';
+import './css/app.css';
 import { MobileContext } from './components/infoview/context';
 import { useWindowDimensions } from './window_width';
-import { selectOpenedIntro } from './state/progress';
-import { useSelector } from 'react-redux';
 
 export const GameIdContext = React.createContext<string>(undefined);
 
 function App() {
   const params = useParams()
   const gameId = "g/" + params.owner + "/" + params.repo
-
-  // TODO: Make mobileLayout be changeable in settings
-  // TODO: Handle resize Events
   const {width, height} = useWindowDimensions()
   const [mobile, setMobile] = React.useState(width < 800)
 
-  // On mobile, there are multiple pages on the welcome page to switch between
-  const openedIntro = useSelector(selectOpenedIntro(gameId))
-  // On mobile, there are multiple pages to switch between
-  const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0)
-
   return (
     <div className="app">
       <GameIdContext.Provider value={gameId}>
-        <MobileContext.Provider value={{mobile, setMobile, pageNumber, setPageNumber}}>
+        <MobileContext.Provider value={{mobile, setMobile}}>
           <Outlet />
         </MobileContext.Provider>
       </GameIdContext.Provider>

client/src/components/app_bar.tsx

@@ -1,45 +1,45 @@
+/**
+ *  @file contains the navigation bars of the app.
+ */
 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 } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from "../app"
 import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context"
 import { GameInfo, useGetGameInfoQuery } from '../state/api'
 import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress } from '../state/progress'
-import { useSelector } from 'react-redux'
 import { useAppDispatch, useAppSelector } from '../hooks'
 import { Button } from './button'
-import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faDownload, faUpload, faEraser, faBook, faGlobe, faHome, faArrowRight, faArrowLeft, faXmark, faBars, faCode, faCircleInfo, faTerminal } from '@fortawesome/free-solid-svg-icons'
-import { PrivacyPolicyPopup } from './privacy_policy'
-import { WorldSelectionMenu, downloadFile } from './world_tree'
+import { downloadProgress } from './popup/erase'
 
-/** navigation to switch between pages on mobile */
-function MobileNav({pageNumber, setPageNumber}:
+/** navigation buttons for mobile welcome page to switch between intro/tree/inventory. */
+function MobileNavButtons({pageNumber, setPageNumber}:
   { pageNumber: number,
     setPageNumber: any}) {
   const gameId = React.useContext(GameIdContext)
   const dispatch = useAppDispatch()
 
-  let prevText = {0 : null, 1: "Intro", 2: null}[pageNumber]
-  let prevIcon = {0 : null, 1: null, 2: faXmark}[pageNumber]
-  let prevTitle = {
-    0: null,
-    1: "Game Introduction",
-    2: "World selection"}[pageNumber]
-  let nextText = {0 : "Start", 1: null, 2: null}[pageNumber]
-  let nextIcon = {0 : null, 1: faBook, 2: null}[pageNumber]
-  let nextTitle = {
-    0: "World selection",
-    1: "Inventory",
-    2: null}[pageNumber]
+  // if `prevText` or `prevIcon` is set, show a button to go back
+  let prevText  = {0: null, 1: "Intro", 2: null}[pageNumber]
+  let prevIcon  = {0: null, 1: null, 2: faBookOpen}[pageNumber]
+  let prevTitle = {0: null, 1: "Game Introduction", 2: "World selection"}[pageNumber]
+  // if `nextText` or `nextIcon` is set, show a button to go forward
+  let nextText  = {0: "Start", 1: null, 2: null}[pageNumber]
+  let nextIcon  = {0: null, 1: faBook, 2: null}[pageNumber]
+  let nextTitle = {0: "World selection", 1: "Inventory", 2: null}[pageNumber]
 
   return <>
-    {(prevText || prevTitle || prevIcon) &&
-      <Button className="btn btn-inverted toggle-width" to={pageNumber == 0 ? "/" : ""} inverted="true" title={prevTitle}
+    {(prevText || prevIcon) &&
+      <Button className="btn btn-inverted toggle-width" to={pageNumber == 0 ? "/" : ""}
+          inverted="true" title={prevTitle}
           onClick={() => {pageNumber == 0 ? null : setPageNumber(pageNumber - 1)}}>
         {prevIcon && <FontAwesomeIcon icon={prevIcon} />}
         {prevText && `${prevText}`}
       </Button>
     }
-    {(nextText || nextTitle || nextIcon) &&
+    {(nextText || nextIcon) &&
       <Button className="btn btn-inverted toggle-width" to="" inverted="true"
           title={nextTitle} onClick={() => {
             console.log(`page number: ${pageNumber}`)
@@ -52,349 +52,203 @@ function MobileNav({pageNumber, setPageNumber}:
   </>
 }
 
-export function WelcomeAppBar({gameInfo, toggleImpressum, openEraseMenu, openUploadMenu, toggleInfo} : {
+/** button to toggle dropdown menu. */
+function MenuButton({navOpen, setNavOpen}) {
+  return <Button to="" className="btn toggle-width" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}}>
+    {navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />}
+  </Button>
+}
+
+/** button to go one level futher.
+ * for the last level, this button turns into a button going back to the welcome page.
+ */
+function NextButton({worldSize, difficulty, completed, setNavOpen}) {
+  const gameId = React.useContext(GameIdContext)
+  const {worldId, levelId} = React.useContext(WorldLevelIdContext)
+  return (levelId < worldSize ?
+    <Button inverted="true"
+        to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title="next level"
+        disabled={difficulty >= 2 && !(completed || levelId == 0)}
+        onClick={() => setNavOpen(false)}>
+      <FontAwesomeIcon icon={faArrowRight} />&nbsp;{levelId ? "Next" : "Start"}
+    </Button>
+    :
+    <Button to={`/${gameId}`} inverted="true" title="back to world selection" id="home-btn">
+      <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
+    </Button>
+  )
+}
+
+/** button to go one level back.
+ * only renders if the current level id is > 0.
+ */
+function PreviousButton({setNavOpen}) {
+  const gameId = React.useContext(GameIdContext)
+  const {worldId, levelId} = React.useContext(WorldLevelIdContext)
+  return (levelId > 0 && <>
+    <Button disabled={levelId <= 0} inverted="true"
+        to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
+        title="previous level"
+        onClick={() => setNavOpen(false)}>
+      <FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
+    </Button>
+  </>)
+}
+
+/** button to toggle between editor and typewriter */
+function InputModeButton({setNavOpen, isDropdown}) {
+  const {levelId} = React.useContext(WorldLevelIdContext)
+  const {typewriterMode, setTypewriterMode, lockInputMode} = React.useContext(InputModeContext)
+
+  /** toggle input mode if allowed */
+  function toggleInputMode(ev: React.MouseEvent) {
+    if (!lockInputMode){
+      setTypewriterMode(!typewriterMode)
+      setNavOpen(false)
+    }
+  }
+
+  return <Button
+      className={`btn btn-inverted ${isDropdown? '' : 'toggle-width'}`} disabled={levelId <= 0 || lockInputMode}
+      inverted="true" to=""
+      onClick={(ev) => toggleInputMode(ev)}
+      title={lockInputMode ? "Editor mode is enforced!" : typewriterMode ? "Editor mode" : "Typewriter mode"}>
+    <FontAwesomeIcon icon={typewriterMode ? faCode : faTerminal} />
+    {isDropdown && (typewriterMode ? <>&nbsp;Editor mode</> : <>&nbsp;Typewriter mode</>)}
+  </Button>
+}
+
+/** button to toggle iimpressum popup */
+function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) {
+  return <Button className="btn btn-inverted toggle-width"
+    title="information, Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
+    <FontAwesomeIcon icon={faCircleInfo} />
+    {isDropdown && <>&nbsp;Info &amp; Impressum</>}
+  </Button>
+}
+
+/**  button to go back to welcome page */
+function HomeButton({isDropdown}) {
+  const gameId = React.useContext(GameIdContext)
+  return <Button to={`/${gameId}`} inverted="true" title="back to world selection" id="home-btn">
+    <FontAwesomeIcon icon={faHome} />
+    {isDropdown && <>&nbsp;Home</>}
+  </Button>
+}
+
+/** button in mobile level to toggle inventory.
+ * only displays a button if `setPageNumber` is set.
+ */
+function InventoryButton({pageNumber, setPageNumber}) {
+  return (setPageNumber &&
+    <Button to="" className="btn btn-inverted toggle-width"
+      title={pageNumber ? "close inventory" : "show inventory"}
+      inverted="true" onClick={() => {setPageNumber(pageNumber ? 0 : 1)}}>
+      <FontAwesomeIcon icon={pageNumber ? faBookOpen : faBook} />
+    </Button>
+  )
+}
+
+/** the navigation bar on the welcome page */
+export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo} : {
+  pageNumber: number,
+  setPageNumber: any,
   gameInfo: GameInfo,
   toggleImpressum: any,
-  openEraseMenu: any,
-  openUploadMenu: any,
+  toggleEraseMenu: any,
+  toggleUploadMenu: any,
   toggleInfo: any
 }) {
   const gameId = React.useContext(GameIdContext)
-  const {mobile, pageNumber, setPageNumber} = React.useContext(MobileContext)
+  const gameProgress = useAppSelector(selectProgress(gameId))
+  const {mobile} = React.useContext(MobileContext)
   const [navOpen, setNavOpen] = React.useState(false)
 
-
-
-  /** Download the current progress (i.e. what's saved in the browser store) */
-  const gameProgress = useSelector(selectProgress(gameId))
-  const downloadProgress = (e) => {
-    e.preventDefault()
-    downloadFile({
-      data: JSON.stringify(gameProgress, null, 2),
-      fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
-      fileType: 'text/json',
-    })
-  }
-
-
-  return   <div className="app-bar" >
-    <>
-      <div>
-        <Button inverted="false" title="back to games selection" to="/">
-          <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
-        </Button>
-        <span className="app-bar-title"></span>
-      </div>
-      <div>
-        <span className="app-bar-title">
-          {mobile ? '' : gameInfo?.title}
-        </span>
-      </div>
-      <div className="nav-btns">
-        {mobile && <>
-          {/* BUTTONS for MOBILE */}
-          <MobileNav pageNumber={pageNumber} setPageNumber={setPageNumber} />
-
-        </>}
-
-        <Button to="" className="btn toggle-width" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}} >
-          {navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />}
-        </Button>
-
-      </div>
-      <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
-        {/* {levelId < gameInfo.data?.worldSize[worldId] &&
-          <Button inverted="true"
-              to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title="next level"
-              disabled={difficulty >= 2 && !(completed || levelId == 0)}
-              onClick={() => setNavOpen(false)}>
-            <FontAwesomeIcon icon={faArrowRight} />&nbsp;{levelId ? "Next" : "Start"}
-          </Button>
-        }
-        {levelId > 0 && <>
-              <Button disabled={levelId <= 0} inverted="true"
-                  to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
-                  title="previous level"
-                  onClick={() => setNavOpen(false)}>
-                <FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
-              </Button>
-            </>}
-        <Button to={`/${gameId}`} inverted="true" title="back to world selection">
-          <FontAwesomeIcon icon={faHome} />&nbsp;Home
-        </Button>
-        <Button disabled={levelId <= 0} inverted="true" to=""
-            onClick={(ev) => { setCommandLineMode(!commandLineMode); setNavOpen(false) }}
-            title="toggle Editor mode">
-          <FontAwesomeIcon icon={faCode} />&nbsp;Toggle Editor
-        </Button> */}
-
-        <Button title="Game Info & Credits" inverted="true" to="" onClick={(ev) => {toggleInfo(); setNavOpen(false)}}>
-          <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Game Info
-        </Button>
-        <Button title="Clear Progress" inverted="true" to="" onClick={(ev) => {openEraseMenu(); setNavOpen(false)}}>
-          <FontAwesomeIcon icon={faEraser} />&nbsp;Erase
-        </Button>
-        <Button title="Download Progress" inverted="true" to="" onClick={(ev) => {downloadProgress(ev); setNavOpen(false)}}>
-          <FontAwesomeIcon icon={faDownload} />&nbsp;Download
-        </Button>
-        <Button title="Load Progress from JSON" inverted="true" to="" onClick={(ev) => {openUploadMenu(); setNavOpen(false)}}>
-          <FontAwesomeIcon icon={faUpload} />&nbsp;Upload
-        </Button>
-        <Button title="Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(); setNavOpen(false)}}>
-          <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Impressum
-        </Button>
-      </div>
-    </>
+  return <div className="app-bar">
+    <div>
+      <Button inverted="false" title="back to games selection" to="/">
+        <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
+      </Button>
+      <span className="app-bar-title"></span>
+    </div>
+    <div>
+      {!mobile && <span className="app-bar-title">{gameInfo?.title}</span>}
+    </div>
+    <div className="nav-btns">
+      {mobile && <MobileNavButtons pageNumber={pageNumber} setPageNumber={setPageNumber} />}
+      <MenuButton navOpen={navOpen} setNavOpen={setNavOpen} />
+    </div>
+    <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
+      <Button title="Game Info & Credits" inverted="true" to="" onClick={() => {toggleInfo(); setNavOpen(false)}}>
+        <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Game Info
+      </Button>
+      <Button title="Clear Progress" inverted="true" to="" onClick={() => {toggleEraseMenu(); setNavOpen(false)}}>
+        <FontAwesomeIcon icon={faEraser} />&nbsp;Erase
+      </Button>
+      <Button title="Download Progress" inverted="true" to="" onClick={(ev) => {downloadProgress(gameId, gameProgress, ev); setNavOpen(false)}}>
+        <FontAwesomeIcon icon={faDownload} />&nbsp;Download
+      </Button>
+      <Button title="Load Progress from JSON" inverted="true" to="" onClick={() => {toggleUploadMenu(); setNavOpen(false)}}>
+        <FontAwesomeIcon icon={faUpload} />&nbsp;Upload
+      </Button>
+      <Button title="Impressum, privacy policy" inverted="true" to="" onClick={() => {toggleImpressum(); setNavOpen(false)}}>
+        <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Impressum
+      </Button>
+    </div>
   </div>
-
-
-
 }
 
-// /** The menu that is shown next to the world selection graph */
-// function WorldSelectionMenu() {
-//   const [file, setFile] = React.useState<File>();
-
-//   const gameId = React.useContext(GameIdContext)
-//   const store = useStore()
-//   const difficulty = useSelector(selectDifficulty(gameId))
-
-
-//   /* state variables to toggle the pop-up menus */
-//   const [eraseMenu, setEraseMenu] = React.useState(false);
-//   const openEraseMenu = () => setEraseMenu(true);
-//   const closeEraseMenu = () => setEraseMenu(false);
-//   const [uploadMenu, setUploadMenu] = React.useState(false);
-//   const openUploadMenu = () => setUploadMenu(true);
-//   const closeUploadMenu = () => setUploadMenu(false);
-
-//   const gameProgress = useSelector(selectProgress(gameId))
-//   const dispatch = useAppDispatch()
-
-//   /** Download the current progress (i.e. what's saved in the browser store) */
-//   const downloadProgress = (e) => {
-//     e.preventDefault()
-//     downloadFile({
-//       data: JSON.stringify(gameProgress, null, 2),
-//       fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
-//       fileType: 'text/json',
-//     })
-//   }
-
-//   const handleFileChange = (e) => {
-//     if (e.target.files) {
-//       setFile(e.target.files[0])
-//     }
-//   }
-
-//   /** Upload progress from a  */
-//   const uploadProgress = (e) => {
-//     if (!file) {return}
-//     const fileReader = new FileReader()
-//     fileReader.readAsText(file, "UTF-8")
-//     fileReader.onload = (e) => {
-//       const data = JSON.parse(e.target.result.toString()) as GameProgressState
-//       console.debug("Json Data", data)
-//       dispatch(loadProgress({game: gameId, data: data}))
-//     }
-//     closeUploadMenu()
-//   }
-
-//   const eraseProgress = () => {
-//     dispatch(deleteProgress({game: gameId}))
-//     closeEraseMenu()
-//   }
-
-//   const downloadAndErase = (e) => {
-//     downloadProgress(e)
-//     eraseProgress()
-//   }
-
-//   function label(x : number) {
-//     return x == 0 ? 'none' : x == 1 ? 'lax' : 'regular'
-//   }
-
-//   return <nav className="world-selection-menu">
-//     <Button onClick={downloadProgress} title="Download game progress" to=""><FontAwesomeIcon icon={faDownload} /></Button>
-//     <Button title="Load game progress from JSON" onClick={openUploadMenu} to=""><FontAwesomeIcon icon={faUpload} /></Button>
-//     <Button title="Clear game progress" to="" onClick={openEraseMenu}><FontAwesomeIcon icon={faEraser} /></Button>
-//     <div className="slider-wrap">
-//       <span className="difficulty-label">Game Rules:</span>
-//       <Slider
-//         title="Game Rules:&#10;- regular: 🔐 levels, 🔐 tactics&#10;- lax: 🔓 levels, 🔐 tactics&#10;- none: 🔓 levels, 🔓 tactics"
-//         min={0} max={2}
-//         aria-label="Game Rules"
-//         defaultValue={difficulty}
-//         marks={[
-//           {value: 0, label: label(0)},
-//           {value: 1, label: label(1)},
-//           {value: 2, label: label(2)}
-//         ]}
-//         valueLabelFormat={label}
-//         getAriaValueText={label}
-//         valueLabelDisplay="auto"
-//         onChange={(ev, val: number) => {
-//           dispatch(changedDifficulty({game: gameId, difficulty: val}))
-//         }}
-//         ></Slider>
-
-//     </div>
-//     {eraseMenu?
-//       <div className="modal-wrapper">
-//         <div className="modal-backdrop" onClick={closeEraseMenu} />
-//         <div className="modal">
-//           <div className="codicon codicon-close modal-close" onClick={closeEraseMenu}></div>
-//           <h2>Delete Progress?</h2>
-
-//           <p>Do you want to delete your saved progress irreversibly?</p>
-//           <p>
-//             (This deletes your proofs and your collected inventory.
-//             Saves from other games are not deleted.)
-//           </p>
-
-//           <Button onClick={eraseProgress} to="">Delete</Button>
-//           <Button onClick={downloadAndErase} to="">Download & Delete</Button>
-//           <Button onClick={closeEraseMenu} to="">Cancel</Button>
-//         </div>
-//       </div> : null}
-//     {uploadMenu ?
-//       <div className="modal-wrapper">
-//         <div className="modal-backdrop" onClick={closeUploadMenu} />
-//         <div className="modal">
-//           <div className="codicon codicon-close modal-close" onClick={closeUploadMenu}></div>
-//           <h2>Upload Saved Progress</h2>
-
-//           <p>Select a JSON file with the saved game progress to load your progress.</p>
-
-//           <p><b>Warning:</b> This will delete your current game progress!
-//             Consider <a className="download-link" onClick={downloadProgress} >downloading your current progress</a> first!</p>
-
-//           <input type="file" onChange={handleFileChange}/>
-
-//           <Button to="" onClick={uploadProgress}>Load selected file</Button>
-//         </div>
-//       </div> : null}
-//   </nav>
-// }
-
-
-/** The top-navigation bar */
-export function LevelAppBar({
-    isLoading, levelTitle, impressum, toggleImpressum,
-    pageNumber = undefined, setPageNumber = undefined}) {
+/** the navigation bar in a level */
+export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=undefined, setPageNumber=undefined} : {
+  isLoading: boolean,
+  levelTitle: string,
+  toggleImpressum: any,
+  pageNumber?: number,
+  setPageNumber?: any,
+}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
-  const gameInfo = useGetGameInfoQuery({game: gameId})
-
   const {mobile} = React.useContext(MobileContext)
-
-  const difficulty = useSelector(selectDifficulty(gameId))
-  const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
-
-  const { commandLineMode, setCommandLineMode } = React.useContext(InputModeContext)
-
   const [navOpen, setNavOpen] = React.useState(false)
+  const gameInfo = useGetGameInfoQuery({game: gameId})
+  const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
+  const difficulty = useAppSelector(selectDifficulty(gameId))
+
+  let worldTitle = gameInfo.data?.worlds.nodes[worldId].title
 
   return <div className="app-bar" style={isLoading ? {display: "none"} : null} >
     {mobile ?
       <>
         {/* MOBILE VERSION */}
         <div>
-          <span className="app-bar-title">
-            {levelTitle}
-          </span>
+          <span className="app-bar-title">{levelTitle}</span>
         </div>
         <div className="nav-btns">
-          {mobile && pageNumber == 0 ?
-            <Button to="" className="btn btn-inverted toggle-width"
-                title="show inventory" inverted="true" onClick={() => {setPageNumber(1)}}>
-              <FontAwesomeIcon icon={faBook}/>
-            </Button>
-          : pageNumber == 1 &&
-            <Button className="btn btn-inverted toggle-width" to=""
-                title="show inventory" inverted="true" onClick={() => {setPageNumber(0)}}>
-              <FontAwesomeIcon icon={faXmark}/>
-            </Button>
-          }
-          <Button to="" className="btn toggle-width" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}} >
-            {navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />}
-          </Button>
+          <InventoryButton pageNumber={pageNumber} setPageNumber={setPageNumber}/>
+          <MenuButton navOpen={navOpen} setNavOpen={setNavOpen}/>
         </div>
         <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
-          {levelId < gameInfo.data?.worldSize[worldId] &&
-            <Button inverted="true"
-                to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title="next level"
-                disabled={difficulty >= 2 && !(completed || levelId == 0)}
-                onClick={() => setNavOpen(false)}>
-              <FontAwesomeIcon icon={faArrowRight} />&nbsp;{levelId ? "Next" : "Start"}
-            </Button>
-          }
-          {levelId > 0 && <>
-                <Button disabled={levelId <= 0} inverted="true"
-                    to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
-                    title="previous level"
-                    onClick={() => setNavOpen(false)}>
-                  <FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
-                </Button>
-              </>}
-          <Button to={`/${gameId}`} inverted="true" title="back to world selection">
-            <FontAwesomeIcon icon={faHome} />&nbsp;Home
-          </Button>
-          <Button disabled={levelId <= 0} inverted="true" to=""
-              onClick={(ev) => { setCommandLineMode(!commandLineMode); setNavOpen(false) }}
-              title="toggle Editor mode">
-            <FontAwesomeIcon icon={faCode} />&nbsp;Toggle Editor
-          </Button>
-          <Button title="information, Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
-            <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Info &amp; Impressum
-          </Button>
+          <NextButton worldSize={gameInfo.data?.worldSize[worldId]} difficulty={difficulty} completed={completed} setNavOpen={setNavOpen} />
+          <PreviousButton setNavOpen={setNavOpen} />
+          <HomeButton isDropdown={true} />
+          <InputModeButton setNavOpen={setNavOpen} isDropdown={true}/>
+          <ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
         </div>
-      </>
-    :
+      </> :
       <>
         {/* DESKTOP VERSION */}
         <div>
-          <Button to={`/${gameId}`} inverted="true" title="back to world selection" id="home-btn">
-            <FontAwesomeIcon icon={faHome} />
-          </Button>
-          <span className="app-bar-title">
-            {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`}
-          </span>
+          <HomeButton isDropdown={false} />
+          <span className="app-bar-title">{worldTitle && `World: ${worldTitle}`}</span>
         </div>
         <div>
-          <span className="app-bar-title">
-            {levelTitle}
-          </span>
+          <span className="app-bar-title">{levelTitle}</span>
         </div>
         <div className="nav-btns">
-          {levelId > 0 && <>
-            <Button disabled={levelId <= 0} inverted="true"
-                to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
-                title="previous level"
-                onClick={() => setNavOpen(false)}>
-              <FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
-            </Button>
-          </>}
-          {levelId < gameInfo.data?.worldSize[worldId] ?
-            <Button inverted="true"
-                to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title="next level"
-                disabled={difficulty >= 2 && !(completed || levelId == 0)}
-                onClick={() => setNavOpen(false)}>
-              <FontAwesomeIcon icon={faArrowRight} />&nbsp;{levelId ? "Next" : "Start"}
-            </Button>
-            :
-            <Button to={`/${gameId}`} inverted="true" title="back to world selection" id="home-btn">
-              <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
-            </Button>
-          }
-          <Button className="btn btn-inverted toggle-width" disabled={levelId <= 0} inverted="true" to=""
-              onClick={(ev) => { setCommandLineMode(!commandLineMode); setNavOpen(false) }}
-              title="toggle Editor mode">
-            <FontAwesomeIcon icon={commandLineMode ? faCode : faTerminal} />
-          </Button>
-          <Button className="btn btn-inverted toggle-width" title="information, Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
-            <FontAwesomeIcon icon={impressum ? faXmark : faCircleInfo} />
-          </Button>
+          <PreviousButton setNavOpen={setNavOpen} />
+          <NextButton worldSize={gameInfo.data?.worldSize[worldId]} difficulty={difficulty} completed={completed} setNavOpen={setNavOpen} />
+          <InputModeButton setNavOpen={setNavOpen} isDropdown={false}/>
+          <ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={false} />
         </div>
       </>
     }

client/src/components/infoview/context.ts

@@ -65,13 +65,9 @@ export const ProofStateContext = React.createContext<{
 export const MobileContext = React.createContext<{
   mobile : boolean,
   setMobile: React.Dispatch<React.SetStateAction<Boolean>>,
-  pageNumber: number,
-  setPageNumber: React.Dispatch<React.SetStateAction<Number>>
 }>({
   mobile : false,
   setMobile: () => {},
-  pageNumber: 0,
-  setPageNumber: () => {}
 })
 
 export const WorldLevelIdContext = React.createContext<{
@@ -105,13 +101,17 @@ export const DeletedChatContext = React.createContext<{
 })
 
 export const InputModeContext = React.createContext<{
-  commandLineMode: boolean,
-  setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>,
-  commandLineInput: string,
-  setCommandLineInput: React.Dispatch<React.SetStateAction<string>>
+  typewriterMode: boolean,
+  setTypewriterMode: React.Dispatch<React.SetStateAction<boolean>>,
+  typewriterInput: string,
+  setTypewriterInput: React.Dispatch<React.SetStateAction<string>>,
+  lockInputMode: boolean,
+  setLockInputMode: React.Dispatch<React.SetStateAction<boolean>>,
 }>({
-  commandLineMode: true,
-  setCommandLineMode: () => {},
-  commandLineInput: "",
-  setCommandLineInput: () => {},
+  typewriterMode: true,
+  setTypewriterMode: () => {},
+  typewriterInput: "",
+  setTypewriterInput: () => {},
+  lockInputMode: false,
+  setLockInputMode: () => {},
 });

client/src/components/infoview/goals.tsx

@@ -124,7 +124,7 @@ interface GoalProps {
     goal: InteractiveGoal
     filter: GoalFilterState
     showHints?: boolean
-    commandLine: boolean
+    typewriter: boolean
 }
 
 interface ProofDisplayProps {
@@ -136,7 +136,7 @@ interface ProofDisplayProps {
  * Displays the hypotheses, target type and optional case label of a goal according to the
  * provided `filter`. */
 export const Goal = React.memo((props: GoalProps) => {
-    const { goal, filter, showHints, commandLine } = props
+    const { goal, filter, showHints, typewriter } = props
 
     // TODO: Apparently `goal` can be `undefined`
     if (!goal) {return <></>}
@@ -163,18 +163,18 @@ export const Goal = React.memo((props: GoalProps) => {
     // const hints = <Hints hints={goal.hints} key={goal.mvarId} />
     const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
     const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
-    const {commandLineMode} = React.useContext(InputModeContext)
+    const {typewriterMode} = React.useContext(InputModeContext)
 
     return <div>
         {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
         {filter.reverse && goalLi}
-        {! commandLine && objectHyps.length > 0 &&
+        {! typewriter && objectHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">Objects:</div>
             {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
-        {!commandLine && assumptionHyps.length > 0 &&
+        {!typewriter && assumptionHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">Assumptions:</div>
             {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
-        {/* {commandLine && commandLineMode && <CommandLine />} */}
+        {/* {typewriter && typewriterMode && <Typewriter />} */}
         {!filter.reverse && goalLi}
         {/* {showHints && hints} */}
     </div>
@@ -229,7 +229,7 @@ export const OtherGoals = React.memo((props: GoalProps2) => {
             <summary>
               <InteractiveCode fmt={goal.type} />
             </summary>
-            <Goal commandLine={false} filter={filter} goal={goal} />
+            <Goal typewriter={false} filter={filter} goal={goal} />
           </details>)}
       </div>}
   </>
@@ -264,7 +264,7 @@ export function Goals({ goals, filter }: GoalsProps) {
         return <>No goals</>
     } else {
         return <>
-          {goals.goals.map((g, i) => <Goal commandLine={false} key={i} goal={g} filter={filter} />)}
+          {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g} filter={filter} />)}
         </>
     }
 }

client/src/components/infoview/info.tsx

@@ -129,7 +129,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
           </div>
           <div>
             { goals && (goals.goals.length > 0
-              ? <Goal commandLine={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
+              ? <Goal typewriter={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
               : <div className="goals-section-title">No Goals</div>
             )}
           </div>
@@ -156,7 +156,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                     <div className="goals-section-title">Weitere Goals</div>
 
                     {goals.goals.slice(1).map((goal, i) =>
-                        <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal commandLine={false} filter={goalFilter} goal={goal} /></details>)}
+                        <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal typewriter={false} filter={goalFilter} goal={goal} /></details>)}
                 </div>}
         </LocationsContext.Provider> */}
     </>

client/src/components/infoview/main.tsx

@@ -1,12 +1,13 @@
 /* Partly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/main.tsx */
 
 import * as React from 'react';
+import {useEffect} from 'react';
 import type { DidCloseTextDocumentParams, DidChangeTextDocumentParams, Location, DocumentUri } from 'vscode-languageserver-protocol';
 
 import 'tachyons/css/tachyons.css';
 import '@vscode/codicons/dist/codicon.css';
 import '../../../../node_modules/lean4-infoview/src/infoview/index.css';
-import './infoview.css'
+import '../../css/infoview.css'
 
 import { LeanFileProgressParams, LeanFileProgressProcessingInfo, defaultInfoviewConfig, EditorApi, InfoviewApi } from '@leanprover/infoview-api';
 import { useClientNotificationEffect, useServerNotificationEffect, useEventResult, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util';
@@ -21,14 +22,14 @@ import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { GameIdContext } from '../../app';
 import { useAppDispatch, useAppSelector } from '../../hooks';
 import { LevelInfo } from '../../state/api';
-import { changedInventory, levelCompleted, selectCompleted, selectInventory } from '../../state/progress';
+import { changedInventory, levelCompleted, selectCode, selectCompleted, selectInventory } from '../../state/progress';
 import Markdown from '../markdown';
 
 import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
 import { Goal } from './goals';
-import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './context';
-import { CommandLine, hasErrors, hasInteractiveErrors } from './command_line';
+import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context';
+import { Typewriter, hasErrors, hasInteractiveErrors } from './typewriter';
 import { InteractiveDiagnostic } from '@leanprover/infoview/*';
 import { Button } from '../button';
 import { CircularProgress } from '@mui/material';
@@ -41,19 +42,16 @@ import { Hints } from '../hints';
  */
 export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize }) {
   const ec = React.useContext(EditorContext)
-  const { commandLineMode } = React.useContext(InputModeContext)
+  const { typewriterMode } = React.useContext(InputModeContext)
   return <>
-    <div className={commandLineMode ? 'hidden' : ''}>
-      <ExerciseStatement data={level} />
+    <div className={typewriterMode ? 'hidden' : ''}>
+      <ExerciseStatement data={level} showLeanStatement={true} />
       <div ref={codeviewRef} className={'codeview'}></div>
     </div>
     {ec ?
       <DualEditorMain worldId={worldId} levelId={levelId} level={level} worldSize={worldSize} /> :
       // TODO: Style this if relevant.
-      <>
-        <p>Editor is starting up...</p>
-        <CircularProgress />
-      </>
+      <></>
     }
   </>
 }
@@ -62,7 +60,7 @@ export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize })
 function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: string, levelId: number, level: LevelInfo, worldSize: number }) {
   const ec = React.useContext(EditorContext)
   const gameId = React.useContext(GameIdContext)
-  const { commandLineMode } = React.useContext(InputModeContext)
+  const { typewriterMode } = React.useContext(InputModeContext)
 
   // Mark level as completed when server gives notification
   const dispatch = useAppDispatch()
@@ -70,7 +68,7 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
     '$/game/completed',
     (params: any) => {
       if (ec.events.changedCursorLocation.current &&
-        ec.events.changedCursorLocation.current.uri === params.uri) {
+          ec.events.changedCursorLocation.current.uri === params.uri) {
         dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))
 
         // On completion, add the names of all new items to the local storage
@@ -80,6 +78,11 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
           ...level?.definitions
         ].filter((tile) => tile.new).map((tile) => tile.name)
 
+        // Add the proven statement to the local storage as well.
+        if (level?.statementName != null) {
+          newTiles.push(level?.statementName)
+        }
+
         let inv: string[] = selectInventory(gameId)(store.getState())
 
         // add new items and remove duplicates
@@ -108,10 +111,10 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
         <WithRpcSessions>
           <WithLspDiagnosticsContext>
             <ProgressContext.Provider value={allProgress}>
-              {commandLineMode ?
-                <CommandLineInterface world={worldId} level={levelId} data={level} worldSize={worldSize}/>
+              {typewriterMode ?
+                <TypewriterInterfaceWrapper world={worldId} level={levelId} data={level} worldSize={worldSize}/>
                 :
-                <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />
+                <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} data={level} />
               }
             </ProgressContext.Provider>
           </WithLspDiagnosticsContext>
@@ -126,22 +129,45 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
  * - Theorem xyz: description
  * - Theorem xyz
  * - Exercises: description
+ *
+ * If `showLeanStatement` is true, it will additionally display the lean code.
  */
-function ExerciseStatement({ data }) {
-  if (!data?.descrText) { return <></> }
-  return <div className="exercise-statement"><Markdown>
-    {(data?.statementName ? `**Theorem** \`${data?.statementName}\`: ` : data?.descrText && "**Exercise**: ") + `${data?.descrText}`}
-  </Markdown></div>
+function ExerciseStatement({ data, showLeanStatement = false }) {
+  if (!(data?.descrText || data?.descrFormat)) { return <></> }
+  return <>
+    <div className="exercise-statement">
+      {data?.descrText &&
+        <Markdown>
+          {(data?.displayName ? `**Theorem** \`${data?.displayName}\`: ` : '') + data?.descrText}
+        </Markdown>
+      }
+      {data?.descrFormat && showLeanStatement &&
+        <p><code className="lean-code">{data?.descrFormat}</code></p>
+      }
+    </div>
+  </>
 }
 
 // TODO: This is only used in `EditorInterface`
-// while `CommandLineInterface` has this copy-pasted in.
-export function Main(props: { world: string, level: number }) {
+// while `TypewriterInterface` has this copy-pasted in.
+export function Main(props: { world: string, level: number, data: LevelInfo}) {
   const ec = React.useContext(EditorContext);
   const gameId = React.useContext(GameIdContext)
+  const {worldId, levelId} = React.useContext(WorldLevelIdContext)
 
   const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
 
+  console.debug(`template: ${props.data.template}`)
+
+  // React.useEffect (() => {
+  //   if (props.data.template) {
+  //     let code: string = selectCode(gameId, worldId, levelId)(store.getState())
+  //     if (!code.length) {
+  //       //models.push(monaco.editor.createModel(code, 'lean4', uri))
+  //     }
+  //   }
+  // }, [props.data.template])
+
   /* Set up updates to the global infoview state on editor events. */
   const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
 
@@ -203,8 +229,8 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
   if (!command) { return <></> }
   return <div className="command">
     <div className="command-text">{command}</div>
-    <Button to="" className="undo-button btn btn-inverted" title="Delete this and future commands" onClick={deleteProof}>
-      <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Delete
+    <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
+      <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
     </Button>
   </div>
 }
@@ -232,7 +258,7 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
 //       message = diag.message
 //   }
 
-//   const { commandLineMode } = React.useContext(InputModeContext)
+//   const { typewriterMode } = React.useContext(InputModeContext)
 
 //   return (
 //   // <details open>
@@ -251,7 +277,7 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
 //       //     </span>
 //       // </summary>
 //       <div className={severityClass + ' ml1 message'}>
-//           {!commandLineMode && <p className="mv2">{title}</p>}
+//           {!typewriterMode && <p className="mv2">{title}</p>}
 //           <pre className="font-code pre-wrap">
 //               <InteractiveMessage fmt={message} />
 //           </pre>
@@ -261,66 +287,124 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
 // }, fastIsEqual)
 
 /** The tabs of goals that lean ahs after the command of this step has been processed */
-function GoalsTab({ proofStep, last}: { proofStep: ProofStep, last : boolean }) {
+function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: ProofStep, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) {
+
   const [selectedGoal, setSelectedGoal] = React.useState<number>(0)
 
-  if (!proofStep.goals.length) { return <></> }
-
-  return <div>
+  return <div className="goal-tabs" onClick={onClick}>
     <div className={`tab-bar ${last ? 'current' : ''}`}>
       {proofStep.goals.map((goal, i) => (
         // TODO: Should not use index as key.
-        <div key={`proof-goal-${i}`} className={`tab ${i == (selectedGoal) ? "active" : ""}`} onClick={(ev) => { setSelectedGoal(i); ev.stopPropagation() }}>
+        <div key={`proof-goal-${i}`} className={`tab ${i == (selectedGoal) ? "active" : ""}`} onClick={(ev) => { onGoalChange(i); setSelectedGoal(i); ev.stopPropagation() }}>
           {i ? `Goal ${i + 1}` : "Active Goal"}
         </div>
       ))}
     </div>
     <div className="goal-tab vscode-light">
-      <Goal commandLine={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]} />
+      <Goal typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]} />
     </div>
   </div>
 }
 
-/** The interface in command line mode */
-export function CommandLineInterface(props: { world: string, level: number, data: LevelInfo, worldSize: number }) {
-
+// Splitting up Typewriter into two parts is a HACK
+export function TypewriterInterfaceWrapper(props: { world: string, level: number, data: LevelInfo, worldSize: number }) {
   const ec = React.useContext(EditorContext)
-  const editor = React.useContext(MonacoEditorContext)
-  const model = editor.getModel()
-  const uri = model.uri.toString()
   const gameId = React.useContext(GameIdContext)
+
+  useClientNotificationEffect(
+    'textDocument/didClose',
+    (params: DidCloseTextDocumentParams) => {
+      if (ec.events.changedCursorLocation.current &&
+        ec.events.changedCursorLocation.current.uri === params.textDocument.uri) {
+        ec.events.changedCursorLocation.fire(undefined)
+      }
+    }, []
+  )
+
+  const serverVersion =
+    useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? ''))
+  const serverStoppedResult = useEventResult(ec.events.serverStopped);
+  // NB: the cursor may temporarily become `undefined` when a file is closed. In this case
+  // it's important not to reconstruct the `WithBlah` wrappers below since they contain state
+  // that we want to persist.
+
+  // Catch loss of internet connection
+  try {
+    const editor = React.useContext(MonacoEditorContext)
+    const model = editor.getModel()
+    if (!model) {
+      return <p>no internet?</p>
+    }
+  } catch {
+    return <p>no internet??</p>
+  }
+
+  if (!serverVersion) { return <></> }
+  if (serverStoppedResult) {
+    return <div>
+      <p>{serverStoppedResult.message}</p>
+      <p className="error">{serverStoppedResult.reason}</p>
+    </div>
+  }
+
+  return <TypewriterInterface props={props} />
+}
+
+/** Delete all proof lines starting from a given line.
+* Note that the first line (i.e. deleting everything) is `1`!
+*/
+function deleteProof(line: number) {
+  const editor = React.useContext(MonacoEditorContext)
   const { proof } = React.useContext(ProofContext)
-  const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
-  const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
+  const { setSelectedStep } = React.useContext(SelectionContext)
+  const { setDeletedChat, showHelp } = React.useContext(DeletedChatContext)
+  const { setTypewriterInput } = React.useContext(InputModeContext)
 
-  const {mobile} = React.useContext(MobileContext)
-
-  const proofPanelRef = React.useRef<HTMLDivElement>(null)
-
-  /** Delete all proof lines starting from a given line.
-   * Note that the first line (i.e. deleting everything) is `1`!
-   */
-  function deleteProof(line: number) {
-    return (ev) => {
-      let deletedChat: Array<GameHint> = []
-      proof.slice(line).map((step, i) => {
-        // Only add these hidden hints to the deletion stack which were visible
-        deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
-      })
-      setDeletedChat(deletedChat)
-
-      editor.executeEdits("command-line", [{
-        range: monaco.Selection.fromPositions(
-          { lineNumber: line, column: 1 },
-          editor.getModel().getFullModelRange().getEndPosition()
-        ),
-        text: '',
-        forceMoveMarkers: false
-      }])
-      setSelectedStep(undefined)
-      ev.stopPropagation()
+  return (ev) => {
+    if (editor) {
+      const model = editor.getModel()
+      if (model) {
+        let deletedChat: Array<GameHint> = []
+        proof.slice(line).map((step, i) => {
+          // Only add these hidden hints to the deletion stack which were visible
+          deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
+        })
+        setDeletedChat(deletedChat)
+        editor.executeEdits("typewriter", [{
+          range: monaco.Selection.fromPositions(
+            { lineNumber: line, column: 1 },
+            model.getFullModelRange().getEndPosition()
+          ),
+          text: '',
+          forceMoveMarkers: false
+        }])
+        setSelectedStep(undefined)
+        setTypewriterInput(proof[line].command)
+        ev.stopPropagation()
+      }
     }
   }
+}
+
+/** The interface in command line mode */
+export function TypewriterInterface({props}) {
+  const gameId = React.useContext(GameIdContext)
+  const editor = React.useContext(MonacoEditorContext)
+
+  const [disableInput, setDisableInput] = React.useState<boolean>(false)
+  const { showHelp, setShowHelp } = React.useContext(DeletedChatContext)
+  const {mobile} = React.useContext(MobileContext)
+  const { proof } = React.useContext(ProofContext)
+  const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
+
+  const proofPanelRef = React.useRef<HTMLDivElement>(null)
+  const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
+  // const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
+  // const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
+
+  // rpc session
+  // editor, model or uri might be null if connection is broken
+  const rpcSess = useRpcSessionAtPos({uri: editor?.getModel()?.uri?.toString() ?? '', line: 0, character: 0})
 
   function toggleSelectStep(line: number) {
     return (ev) => {
@@ -342,6 +426,11 @@ export function CommandLineInterface(props: { world: string, level: number, data
     } else {
       proofPanelRef.current?.scrollTo(0,0)
     }
+    // also reenable the commandline when the proof changes
+
+    // BUG: If selecting 2nd goal on a intermediate proofstep and then delete proof to there,
+    // the commandline is not displaying disabled even though it should.
+    setDisableInput(false)
   }, [proof])
 
   // Scroll to element if selection changes
@@ -353,37 +442,6 @@ export function CommandLineInterface(props: { world: string, level: number, data
     }
   }, [selectedStep])
 
-  const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
-
-  const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
-
-  const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
-
-  useClientNotificationEffect(
-    'textDocument/didClose',
-    (params: DidCloseTextDocumentParams) => {
-      if (ec.events.changedCursorLocation.current &&
-        ec.events.changedCursorLocation.current.uri === params.textDocument.uri) {
-        ec.events.changedCursorLocation.fire(undefined)
-      }
-    }, []
-  )
-
-  const serverVersion =
-    useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? ''))
-  const serverStoppedResult = useEventResult(ec.events.serverStopped);
-  // NB: the cursor may temporarily become `undefined` when a file is closed. In this case
-  // it's important not to reconstruct the `WithBlah` wrappers below since they contain state
-  // that we want to persist.
-
-  if (!serverVersion) { return <p>Waiting for Lean server to start...</p> }
-  if (serverStoppedResult) {
-    return <div>
-      <p>{serverStoppedResult.message}</p>
-      <p className="error">{serverStoppedResult.reason}</p>
-    </div>
-  }
-
   // TODO: This about hidden hints is all copied from `level.tsx`. Can we move that into `hints.tsx`?
 
   // If the last step has errors, we want to treat it as if it is part of the second-to-last step
@@ -417,16 +475,10 @@ export function CommandLineInterface(props: { world: string, level: number, data
 
   let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : false
 
-  // TODO: does the position matter at all?
-  const rpcSess = useRpcSessionAtPos({uri: uri, line: 0, character: 0})
-
-  return <div className="commandline-interface">
+  return <div className="typewriter-interface">
     <RpcContext.Provider value={rpcSess}>
     <div className="content">
       <div className="tmp-pusher">
-        {!proof.length &&
-          <CircularProgress />
-        }
       </div>
       <div className='proof' ref={proofPanelRef}>
         <ExerciseStatement data={props.data} />
@@ -438,12 +490,12 @@ export function CommandLineInterface(props: { world: string, level: number, data
                 // entered command as it is still present in the command line.
                 // TODO: Should not use index as key.
                 return <div key={`proof-step-${i}`}>
-                  <Errors errors={step.errors} commandLineMode={true} />
+                  <Errors errors={step.errors} typewriterMode={true} />
                 </div>
               } else {
-                return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')} onClick={toggleSelectStep(i)}>
+                return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')}>
                   <Command command={step.command} deleteProof={deleteProof(i)} />
-                  <Errors errors={step.errors} commandLineMode={true} />
+                  <Errors errors={step.errors} typewriterMode={true} />
                   {mobile && i == 0 && props.data?.introduction &&
                     <div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}>
                       <Markdown>{props.data?.introduction}</Markdown>
@@ -460,7 +512,7 @@ export function CommandLineInterface(props: { world: string, level: number, data
                     }
                   </>
                   }
-                  <GoalsTab proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} />
+                  <GoalsTabs proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/>
                   {/* Show a message that there are no goals left */}
                   {!step.goals.length && (
                     <div className="message information">
@@ -489,11 +541,11 @@ export function CommandLineInterface(props: { world: string, level: number, data
                 }
               </div>
             }
-          </> : <></>
+          </> : <CircularProgress />
         }
       </div>
     </div>
-    <CommandLine hidden={!withErr && proof[proof.length - 1]?.goals.length == 0}/>
+    <Typewriter hidden={!withErr && proof[proof.length - 1]?.goals.length == 0} disabled={disableInput || !proof.length}/>
     </RpcContext.Provider>
   </div>
 }

client/src/components/infoview/messages.tsx

@@ -18,7 +18,7 @@ interface MessageViewProps {
 }
 
 /** A list of messages (info/warning/error) that are produced after this command */
-function Error({error, commandLineMode} : {error : InteractiveDiagnostic, commandLineMode : boolean}) {
+function Error({error, typewriterMode} : {error : InteractiveDiagnostic, typewriterMode : boolean}) {
   // The first step will always have an empty command
 
   const severityClass = error.severity ? {
@@ -41,7 +41,7 @@ function Error({error, commandLineMode} : {error : InteractiveDiagnostic, comman
   }
 
   return <div className={severityClass + ' ml1 message'}>
-    {!commandLineMode && <p className="mv2">{title}</p>}
+    {!typewriterMode && <p className="mv2">{title}</p>}
     <pre className="font-code pre-wrap">
       <InteractiveMessage fmt={message} />
     </pre>
@@ -50,9 +50,9 @@ function Error({error, commandLineMode} : {error : InteractiveDiagnostic, comman
 
 // TODO: Should not use index as key.
 /** A list of messages (info/warning/error) that are produced after this command */
-export function Errors ({errors, commandLineMode} : {errors : InteractiveDiagnostic[], commandLineMode : boolean}) {
+export function Errors ({errors, typewriterMode} : {errors : InteractiveDiagnostic[], typewriterMode : boolean}) {
   return <div>
-    {errors.map((err, i) => (<Error key={`error-${i}`} error={err} commandLineMode={commandLineMode}/>))}
+    {errors.map((err, i) => (<Error key={`error-${i}`} error={err} typewriterMode={typewriterMode}/>))}
   </div>
 }
 
@@ -79,7 +79,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         message = diag.message
     }
 
-    const { commandLineMode } = React.useContext(InputModeContext)
+    const { typewriterMode } = React.useContext(InputModeContext)
 
     return (
     // <details open>
@@ -98,7 +98,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         //     </span>
         // </summary>
         <div className={severityClass + ' ml1 message'}>
-            {!commandLineMode && <p className="mv2">{title}</p>}
+            {!typewriterMode && <p className="mv2">{title}</p>}
             <pre className="font-code pre-wrap">
                 <InteractiveMessage fmt={message} />
             </pre>

client/src/components/infoview/typewriter.tsx

@@ -64,17 +64,17 @@ config.autoClosingPairs = config.autoClosingPairs.map(
 monaco.languages.setLanguageConfiguration('lean4cmd', config);
 
 /** The input field */
-export function CommandLine({hidden}: {hidden?: boolean}) {
+export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boolean}) {
 
   /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
-  const model = editor.getModel()
-  const uri = model.uri.toString()
+  const model = editor?.getModel()
+  const uri = model?.uri?.toString()
 
   const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
   const [processing, setProcessing] = useState(false)
 
-  const {commandLineInput, setCommandLineInput} = React.useContext(InputModeContext)
+  const {typewriterInput, setTypewriterInput} = React.useContext(InputModeContext)
 
   const inputRef = useRef()
 
@@ -91,16 +91,20 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
    */
   const loadAllGoals = React.useCallback(() => {
 
+    if (!model || ! uri) {
+      return
+    }
+
     let goalCalls = []
     let msgCalls = []
 
     // For each line of code ask the server for the goals and the messages on this line
-    for (let i = 0; i < model.getLineCount(); i++) {
+    for (let i = 0; i < model?.getLineCount(); i++) {
       goalCalls.push(
         rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
       )
       msgCalls.push(
-        getInteractiveDiagnostics(rpcSess, {start: i, end: i+1})
+        getInteractiveDiagnostics(rpcSess, {start: i, end: i+1}).catch((error) => {console.debug("promise broken")})
       )
     }
 
@@ -158,7 +162,7 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
           // with no goals there will be no hints.
           let hints : GameHint[] = goals.goals.length ? goals.goals[0].hints : []
 
-          console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
+          console.debug(`Command (${i}): `, i ? model?.getLineContent(i) : '')
           console.debug(`Goals: (${i}): `, goalsToString(goals)) //
           console.debug(`Hints: (${i}): `, hints)
           console.debug(`Errors: (${i}): `, messages)
@@ -166,7 +170,7 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
           tmpProof.push({
             // the command of the line above. Note that `getLineContent` starts counting
             // at `1` instead of `zero`. The first ProofStep will have an empty command.
-            command: i ? model.getLineContent(i) : '',
+            command: i ? model?.getLineContent(i) : '',
             // TODO: store correct data
             goals: goals.goals,
             // only need the hints of the active goals in chat
@@ -178,47 +182,57 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
         })
         // Save the proof to the context
         setProof(tmpProof)
-      })
-    })
+      }).catch((error) => {console.debug("promise broken")})
+    }).catch((error) => {console.debug("promise broken")})
   }, [editor, rpcSess, uri, model])
 
   // Run the command
   const runCommand = React.useCallback(() => {
     if (processing) {return}
+    if (!uri) {return}
 
     // TODO: Desired logic is to only reset this after a new *error-free* command has been entered
     setDeletedChat([])
 
     const pos = editor.getPosition()
-    if (commandLineInput) {
+    if (typewriterInput) {
       setProcessing(true)
-      editor.executeEdits("command-line", [{
+      editor.executeEdits("typewriter", [{
         range: monaco.Selection.fromPositions(
           pos,
-          editor.getModel().getFullModelRange().getEndPosition()
+          model.getFullModelRange().getEndPosition()
         ),
-        text: commandLineInput.trim() + "\n",
+        text: typewriterInput.trim() + "\n",
         forceMoveMarkers: false
       }])
+      setTypewriterInput('')
     }
 
     editor.setPosition(pos)
-  }, [commandLineInput, editor])
+  }, [typewriterInput, editor, model])
 
   useEffect(() => {
-    if (oneLineEditor && oneLineEditor.getValue() !== commandLineInput) {
-      oneLineEditor.setValue(commandLineInput)
+    if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) {
+      oneLineEditor.setValue(typewriterInput)
     }
-  }, [commandLineInput])
+  }, [typewriterInput])
+
+  useEffect(() => {
+    if (proof.length && hasInteractiveErrors(proof[proof.length - 1].errors)) {
+      setTypewriterInput(proof[proof.length - 1].command)
+    }
+  }, [proof])
 
   // React when answer from the server comes back
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
+    if (!uri) {return}
+
     if (params.uri == uri) {
       setProcessing(false)
       loadAllGoals()
       if (!hasErrors(params.diagnostics)) {
-        setCommandLineInput("")
-        editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
+        //setTypewriterInput("")
+        editor.setPosition(model.getFullModelRange().getEndPosition())
       }
     } else {
       // console.debug(`expected uri: ${uri}, got: ${params.uri}`)
@@ -227,11 +241,11 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
     // TODO: This is the wrong place apparently. Where do wee need to load them?
     // TODO: instead of loading all goals every time, we could only load the last one
     // loadAllGoals()
-  }, [uri]);
+  }, [uri, editor, model]);
 
   useEffect(() => {
     const myEditor = monaco.editor.create(inputRef.current!, {
-      value: commandLineInput,
+      value: typewriterInput,
       language: "lean4cmd",
       quickSuggestions: false,
       lightbulb: {
@@ -274,14 +288,14 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
     // Ensure that our one-line editor can only have a single line
     const l = oneLineEditor.getModel().onDidChangeContent((e) => {
       const value = oneLineEditor.getValue()
-      setCommandLineInput(value)
+      setTypewriterInput(value)
       const newValue = value.replace(/[\n\r]/g, '')
       if (value != newValue) {
         oneLineEditor.setValue(newValue)
       }
     })
     return () => { l.dispose() }
-  }, [oneLineEditor, setCommandLineInput])
+  }, [oneLineEditor, setTypewriterInput])
 
   useEffect(() => {
     if (!oneLineEditor) return
@@ -297,10 +311,8 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
   // BUG: Causes `file closed` error
   //TODO: Intention is to run once when loading, does that work?
   useEffect(() => {
-    console.debug(`time to update: ${uri} \n ${rpcSess}`)
-    console.debug(rpcSess)
     loadAllGoals()
-  }, [rpcSess])
+  }, [])
 
   /** Process the entered command */
   const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
@@ -308,10 +320,10 @@ export function CommandLine({hidden}: {hidden?: boolean}) {
     runCommand()
   }
 
-  return <div className={`command-line${hidden ? ' hidden' : ''}`}>
+  return <div className={`typewriter${hidden ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
       <form onSubmit={handleSubmit}>
-        <div className="command-line-input-wrapper">
-          <div ref={inputRef} className="command-line-input" />
+        <div className="typewriter-input-wrapper">
+          <div ref={inputRef} className="typewriter-input" />
         </div>
         <button type="submit" disabled={processing} className="btn btn-inverted">
           <FontAwesomeIcon icon={faWandMagicSparkles} /> Execute

client/src/components/inventory.tsx

@@ -1,11 +1,12 @@
 import * as React from 'react';
 import { useState, useEffect } from 'react';
-import './inventory.css'
+import '../css/inventory.css'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-solid-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 { QueryStatus } from '@reduxjs/toolkit/query/react'
 import { selectDifficulty, selectInventory } from '../state/progress';
 import { store } from '../state/store';
 import { useSelector } from 'react-redux';
@@ -29,7 +30,7 @@ export function Inventory({levelInfo, openDoc, enableAll=false} :
       {levelInfo?.definitions &&
         <InventoryList items={levelInfo?.definitions} docType="Definition" openDoc={openDoc} enableAll={enableAll}/>
       }
-      <h2>Lemmas</h2>
+      <h2>Theorems</h2>
       {levelInfo?.lemmas &&
         <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} defaultTab={levelInfo?.lemmaTab} level={levelInfo} enableAll={enableAll}/>
       }
@@ -114,16 +115,32 @@ function InventoryItem({name, displayName, locked, disabled, newly, showDoc, ena
   return <div className={`item ${className}${enableAll ? ' enabled' : ''}`} onClick={handleClick} title={title}>{icon} {displayName}</div>
 }
 
+/** Wrapper to catch rejected/pending queries. */
+function DocContent({doc}) {
+  switch(doc.status) {
+    case QueryStatus.fulfilled:
+      return <>
+        <h1 className="doc">{doc.data.displayName}</h1>
+        <p><code>{doc.data.statement}</code></p>
+        {/* <code>docstring: {doc.data.docstring}</code> */}
+        <Markdown>{doc.data.content}</Markdown>
+      </>
+    case QueryStatus.rejected:
+      return <p>Looks like there is a connection problem!</p>
+    case QueryStatus.pending:
+      return <p>Loading...</p>
+    default:
+      return <></>
+  }
+}
+
 export function Documentation({name, type, handleClose}) {
   const gameId = React.useContext(GameIdContext)
   const doc = useLoadDocQuery({game: gameId, type: type, name: name})
 
   return <div className="documentation">
     <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h1 className="doc">{doc.data?.displayName}</h1>
-    <p><code>{doc.data?.statement}</code></p>
-    {/* <code>docstring: {doc.data?.docstring}</code> */}
-    <Markdown>{doc.data?.content}</Markdown>
+      <DocContent doc={doc} />
   </div>
 }
 

client/src/components/landing_page.tsx

@@ -6,12 +6,12 @@ import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
 
-import './landing_page.css'
+import '../css/landing_page.css'
 import coverRobo from '../assets/covers/formaloversum.png'
 import bgImage from '../assets/bg.jpg'
 
 import Markdown from './markdown';
-import {PrivacyPolicyPopup} from './privacy_policy'
+import {PrivacyPolicyPopup} from './popup/privacy_policy'
 
 const flag = {
   'Dutch': '🇳🇱',
@@ -57,6 +57,7 @@ function GameTile({
       <div className="long description"><Markdown>{description}</Markdown></div>
     </div>
     <table className="info">
+      <tbody>
       <tr>
         <td title="consider playing these games first.">Prerequisites</td>
         <td><Markdown>{prereq}</Markdown></td>
@@ -73,6 +74,7 @@ function GameTile({
         <td>Language</td>
         <td title={`in ${language}`}>{flag[language]}</td>
       </tr>
+      </tbody>
     </table>
   </div>
 
@@ -111,8 +113,8 @@ function LandingPage() {
 learning the basics about theorem proving in Lean.
 
 This is a good first introduction to Lean!"
-        worlds="9"
-        levels="72"
+        worlds="4"
+        levels="30"
         language="English"
         />
 
@@ -128,6 +130,15 @@ Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet
         language="German"
         />
 
+      <GameTile
+        title="NNG (OLD)"
+        gameId="g/hhu-adam/nng4-old"
+        intro="The old version of the NNG copied from lean3."
+        description="This version is not maintained and might break at any point. You should play the new version instead"
+        worlds="9"
+        levels="72"
+        language="English"
+        />
     </div>
     <section>
       <div className="wrapper">
@@ -153,7 +164,7 @@ Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet
           a template.
         </p>
         <p>
-          There is an option to load and run your own games direclty on the server,
+          There is an option to load and run your own games directly on the server,
           instructions are in the NNG repo. Since this is still in development we'd like to
           encourage you to contact us for support creating your own game. The documentation is
           not polished yet.

client/src/components/level.tsx

@@ -4,7 +4,7 @@ import { useSelector, useStore } from 'react-redux'
 import Split from 'react-split'
 import { useParams } from 'react-router-dom'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faBars, faBook, faCode, faXmark, faHome, faCircleInfo, faArrowRight, faArrowLeft, faTerminal } from '@fortawesome/free-solid-svg-icons'
+import { faHome, faArrowRight } from '@fortawesome/free-solid-svg-icons'
 import { CircularProgress } from '@mui/material'
 import type { Location } from 'vscode-languageserver-protocol'
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
@@ -27,13 +27,13 @@ import { store } from '../state/store'
 import { Button } from './button'
 import Markdown from './markdown'
 import {InventoryPanel} from './inventory'
-import { hasInteractiveErrors } from './infoview/command_line'
+import { hasInteractiveErrors } from './infoview/typewriter'
 import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext,
   ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
 import { GameHint } from './infoview/rpc_api'
 import { DeletedHints, Hint, Hints } from './hints'
-import { Impressum } from './privacy_policy'
+import { PrivacyPolicyPopup } from './popup/privacy_policy'
 
 import '@fontsource/roboto/300.css'
 import '@fontsource/roboto/400.css'
@@ -41,7 +41,7 @@ import '@fontsource/roboto/500.css'
 import '@fontsource/roboto/700.css'
 import 'lean4web/client/src/editor/infoview.css'
 import 'lean4web/client/src/editor/vscode.css'
-import './level.css'
+import '../css/level.css'
 import { LevelAppBar } from './app_bar'
 
 function Level() {
@@ -50,8 +50,17 @@ function Level() {
   const worldId = params.worldId
   // useLoadWorldFiles(worldId)
 
+  const [impressum, setImpressum] = React.useState(false)
+
+  const closeImpressum = () => {
+    setImpressum(false)
+  }
+
   return <WorldLevelIdContext.Provider value={{worldId, levelId}}>
-    {levelId == 0 ? <Introduction /> : <PlayableLevel key={`${worldId}/${levelId}`}/>}
+    {levelId == 0 ?
+      <Introduction impressum={impressum} setImpressum={setImpressum} /> :
+      <PlayableLevel key={`${worldId}/${levelId}`} impressum={impressum} setImpressum={setImpressum} />}
+    {impressum ? <PrivacyPolicyPopup handleClose={closeImpressum} /> : null}
   </WorldLevelIdContext.Provider>
 }
 
@@ -127,13 +136,14 @@ function ChatPanel({lastLevel}) {
   //   // chatRef.current!.scrollTo(0,0)
   // }, [gameId, worldId, levelId])
 
+  let introText: Array<string> = level?.data?.introduction.split(/\n(\s*\n)+/)
+
   return <div className="chat-panel">
     <div ref={chatRef} className="chat">
-      {level?.data?.introduction &&
-        <div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelection(0)}>
-          <Markdown>{level?.data?.introduction}</Markdown>
-        </div>
-      }
+      {introText?.filter(t => t.trim()).map(((t, i) =>
+        <Hint key={`intro-p-${i}`}
+          hint={{text: t, hidden: false}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
+      ))}
       {proof.map((step, i) => {
         // It the last step has errors, it will have the same hints
         // as the second-to-last step. Therefore we should not display them.
@@ -176,7 +186,7 @@ function ChatPanel({lastLevel}) {
   </div>
 }
 
-function ExercisePanel({codeviewRef, impressum, closeImpressum, visible=true}) {
+function ExercisePanel({codeviewRef, visible=true}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
@@ -185,11 +195,10 @@ function ExercisePanel({codeviewRef, impressum, closeImpressum, visible=true}) {
     <div className="exercise">
       <DualEditor level={level?.data} codeviewRef={codeviewRef} levelId={levelId} worldId={worldId} worldSize={gameInfo.data?.worldSize[worldId]}/>
     </div>
-    {impressum ? <Impressum handleClose={closeImpressum} /> : null}
   </div>
 }
 
-function PlayableLevel() {
+function PlayableLevel({impressum, setImpressum}) {
   const codeviewRef = useRef<HTMLDivElement>(null)
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
@@ -212,14 +221,14 @@ function PlayableLevel() {
   const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
   // Only for mobile layout
   const [pageNumber, setPageNumber] = useState(0)
-  const [commandLineMode, setCommandLineMode] = useState(true)
-  const [commandLineInput, setCommandLineInput] = useState("")
+  const [typewriterMode, setTypewriterMode] = useState(true)
+  // set to true to prevent switching between typewriter and editor
+  const [lockInputMode, setLockInputMode] = useState(false)
+  const [typewriterInput, setTypewriterInput] = useState("")
   const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
   const dispatch = useAppDispatch()
 
   // impressum pop-up
-  const [impressum, setImpressum] = React.useState(false)
-  function closeImpressum() {setImpressum(false)}
   function toggleImpressum() {setImpressum(!impressum)}
 
   // When clicking on an inventory item, the inventory is overlayed by the item's doc.
@@ -228,8 +237,6 @@ function PlayableLevel() {
   const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
   function closeInventoryDoc () {setInventoryDoc(null)}
 
-
-
   const onDidChangeContent = (code) => {
     dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code}))
   }
@@ -245,30 +252,30 @@ function PlayableLevel() {
   const {editor, infoProvider, editorConnection} =
     useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection)
 
-  /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside
-   * `CommandLineInterface`.
-   */
-  const handleUndo = () => {
-    const endPos = editor.getModel().getFullModelRange().getEndPosition()
-    let range
-    console.log(endPos.column)
-    if (endPos.column === 1) {
-      range = monaco.Selection.fromPositions(
-        new monaco.Position(endPos.lineNumber - 1, 1),
-        endPos
-      )
-    } else {
-      range = monaco.Selection.fromPositions(
-        new monaco.Position(endPos.lineNumber, 1),
-        endPos
-      )
-    }
-    editor.executeEdits("undo-button", [{
-      range,
-      text: "",
-      forceMoveMarkers: false
-    }]);
-  }
+  // /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside
+  //  * `TypewriterInterface`.
+  //  */
+  // const handleUndo = () => {
+  //   const endPos = editor.getModel().getFullModelRange().getEndPosition()
+  //   let range
+  //   console.log(endPos.column)
+  //   if (endPos.column === 1) {
+  //     range = monaco.Selection.fromPositions(
+  //       new monaco.Position(endPos.lineNumber - 1, 1),
+  //       endPos
+  //     )
+  //   } else {
+  //     range = monaco.Selection.fromPositions(
+  //       new monaco.Position(endPos.lineNumber, 1),
+  //       endPos
+  //     )
+  //   }
+  //   editor.executeEdits("undo-button", [{
+  //     range,
+  //     text: "",
+  //     forceMoveMarkers: false
+  //   }]);
+  // }
 
   // Select and highlight proof steps and corresponding hints
   // TODO: with the new design, there is no difference between the introduction and
@@ -278,29 +285,100 @@ function PlayableLevel() {
   // if the user inventory changes, notify the server
   useEffect(() => {
     let leanClient = connection.getLeanClient(gameId)
-    leanClient.sendNotification('$/game/setInventory', {inventory: inventory, checkEnabled: difficulty > 0})
+    leanClient.sendNotification('$/game/setInventory', {inventory: inventory, difficulty: difficulty})
   }, [inventory])
 
+  useEffect (() => {
+    // Lock editor mode
+    if (level?.data?.template) {
+      setTypewriterMode(false)
+
+      if (editor) {
+        let model = editor.getModel()
+        if (model) {
+          let code = model.getLinesContent()
+
+          // console.log(`insert. code: ${code}`)
+          // console.log(`insert. join: ${code.join('')}`)
+          // console.log(`insert. trim: ${code.join('').trim()}`)
+          // console.log(`insert. length: ${code.join('').trim().length}`)
+          // console.log(`insert. range: ${editor.getModel().getFullModelRange()}`)
+
+
+          // TODO: It does seem that the template is always indented by spaces.
+          // This is a hack, assuming there are exactly two.
+          if (!code.join('').trim().length) {
+            console.debug(`inserting template:\n${level.data.template}`)
+            // TODO: This does not work! HERE
+            // Probably overwritten by a query to the server
+            editor.executeEdits("template-writer", [{
+              range: model.getFullModelRange(),
+              text: level.data.template + `\n`,
+              forceMoveMarkers: true
+            }])
+          } else {
+            console.debug(`not inserting template.`)
+          }
+        }
+      }
+    } else {
+      setTypewriterMode(true)
+    }
+  }, [level, levelId, worldId, gameId, editor])
+
+
   useEffect(() => {
     // TODO: That's a problem if the saved proof contains an error
     // Reset command line input when loading a new level
-    setCommandLineInput("")
+    setTypewriterInput("")
 
     // Load the selected help steps from the store
     setShowHelp(new Set(selectHelp(gameId, worldId, levelId)(store.getState())))
   }, [gameId, worldId, levelId])
 
+  // switching editor mode
   useEffect(() => {
-    if (!commandLineMode) {
-      // Delete last input attempt from command line
-      editor.executeEdits("command-line", [{
-        range: editor.getSelection(),
-        text: "",
-        forceMoveMarkers: false
-      }]);
-      editor.focus()
+    if (editor) {
+      let model = editor.getModel()
+      if (model) {
+        if (typewriterMode) {
+          // typewriter gets enabled
+          let code = model.getLinesContent().filter(line => line.trim())
+          editor.executeEdits("typewriter", [{
+            range: model.getFullModelRange(),
+            text: code.length ? code.join('\n') + '\n' : '',
+            forceMoveMarkers: true
+          }])
+
+          // let endPos = model.getFullModelRange().getEndPosition()
+          // if (model.getLineContent(endPos.lineNumber).trim() !== "") {
+          //   editor.executeEdits("typewriter", [{
+          //     range: monaco.Selection.fromPositions(endPos, endPos),
+          //     text: "\n",
+          //     forceMoveMarkers: true
+          //   }]);
+          // }
+          // let endPos = model.getFullModelRange().getEndPosition()
+          // let currPos = editor.getPosition()
+          // if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) {
+          //   // This is not a position that would naturally occur from Typewriter, reset:
+          //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
+          // }
+        } else {
+          // typewriter gets disabled
+          // delete last input attempt from command line
+          editor.executeEdits("typewriter", [{
+            range: editor.getSelection(),
+            text: "",
+            forceMoveMarkers: false
+          }]);
+          editor.focus()
+        }
+      }
+
+
     }
-  }, [commandLineMode])
+  }, [editor, typewriterMode])
 
   useEffect(() => {
     // Forget whether hidden hints are displayed for steps that don't exist yet
@@ -318,48 +396,25 @@ function PlayableLevel() {
     }
   }, [showHelp])
 
-  // Effect when command line mode gets enabled
-  useEffect(() => {
-    if (editor && commandLineMode) {
-      let endPos = editor.getModel().getFullModelRange().getEndPosition()
-      if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
-        editor.executeEdits("command-line", [{
-          range: monaco.Selection.fromPositions(endPos, endPos),
-          text: "\n",
-          forceMoveMarkers: true
-        }]);
-      }
-      endPos = editor.getModel().getFullModelRange().getEndPosition()
-      let currPos = editor.getPosition()
-      if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) {
-        // This is not a position that would naturally occur from CommandLine, reset:
-        editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
-      }
-    }
-  }, [editor, commandLineMode])
-
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
     <DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
       <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
-        <InputModeContext.Provider value={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
+        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockInputMode, setLockInputMode}}>
           <ProofContext.Provider value={{proof, setProof}}>
             <EditorContext.Provider value={editorConnection}>
               <MonacoEditorContext.Provider value={editor}>
                 <LevelAppBar
+                  pageNumber={pageNumber} setPageNumber={setPageNumber}
                   isLoading={level.isLoading}
                   levelTitle={`${mobile ? '' : 'Level '}${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
                     (level?.data?.title && ` : ${level?.data?.title}`)}
-                  impressum={impressum}
-                    toggleImpressum={toggleImpressum}
-                  pageNumber={pageNumber} setPageNumber={setPageNumber} />
+                  toggleImpressum={toggleImpressum} />
                 {mobile?
                   // TODO: This is copied from the `Split` component below...
                   <>
                     <div className={`app-content level-mobile ${level.isLoading ? 'hidden' : ''}`}>
                       <ExercisePanel
-                        impressum={impressum}
-                        closeImpressum={closeImpressum}
                         codeviewRef={codeviewRef}
                         visible={pageNumber == 0} />
                       <InventoryPanel levelInfo={level?.data} visible={pageNumber == 1} />
@@ -369,8 +424,6 @@ function PlayableLevel() {
                   <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
                     <ChatPanel lastLevel={lastLevel}/>
                     <ExercisePanel
-                      impressum={impressum}
-                      closeImpressum={closeImpressum}
                       codeviewRef={codeviewRef} />
                     <InventoryPanel levelInfo={level?.data} />
                   </Split>
@@ -384,7 +437,7 @@ function PlayableLevel() {
   </>
 }
 
-function IntroductionPanel({gameInfo, impressum, closeImpressum}) {
+function IntroductionPanel({gameInfo}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId} = useContext(WorldLevelIdContext)
 
@@ -396,7 +449,6 @@ function IntroductionPanel({gameInfo, impressum, closeImpressum}) {
         <Hint key={`intro-p-${i}`}
           hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
       ))}
-      {impressum ? <Impressum handleClose={closeImpressum} /> : null}
     </div>
     <div className="button-row">
       {gameInfo.data?.worldSize[worldId] == 0 ?
@@ -412,7 +464,7 @@ function IntroductionPanel({gameInfo, impressum, closeImpressum}) {
 export default Level
 
 /** The site with the introduction text of a world */
-function Introduction() {
+function Introduction({impressum, setImpressum}) {
   const gameId = React.useContext(GameIdContext)
   const {mobile} = useContext(MobileContext)
 
@@ -420,56 +472,26 @@ function Introduction() {
 
   const gameInfo = useGetGameInfoQuery({game: gameId})
 
-  const [impressum, setImpressum] = React.useState(false)
-
-  const closeImpressum = () => {
-    setImpressum(false)
-  }
-
   const toggleImpressum = () => {
     setImpressum(!impressum)
   }
 
   return <>
-    <LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Introduction" impressum={impressum} toggleImpressum={toggleImpressum}/>
+    <LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Introduction" toggleImpressum={toggleImpressum}/>
     {gameInfo.isLoading ?
       <div className="app-content loading"><CircularProgress /></div>
     : mobile ?
-        <IntroductionPanel gameInfo={gameInfo} impressum={impressum} closeImpressum={closeImpressum} />
+        <IntroductionPanel gameInfo={gameInfo} />
       :
         <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level`}>
-          <IntroductionPanel gameInfo={gameInfo} impressum={impressum} closeImpressum={closeImpressum} />
+          <IntroductionPanel gameInfo={gameInfo} />
           <div className="world-image-container empty"></div>
           <InventoryPanel levelInfo={inventory?.data} />
         </Split>
       }
-
   </>
 }
 
-// {mobile?
-//   // TODO: This is copied from the `Split` component below...
-//   <>
-//     <div className={`app-content level-mobile ${level.isLoading ? 'hidden' : ''}`}>
-//       <ExercisePanel
-//         impressum={impressum}
-//         closeImpressum={closeImpressum}
-//         codeviewRef={codeviewRef}
-//         visible={pageNumber == 0} />
-//       <InventoryPanel levelInfo={level?.data} visible={pageNumber == 1} />
-//     </div>
-//   </>
-// :
-//   <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
-//     <ChatPanel lastLevel={lastLevel}/>
-//     <ExercisePanel
-//       impressum={impressum}
-//       closeImpressum={closeImpressum}
-//       codeviewRef={codeviewRef} />
-//     <InventoryPanel levelInfo={level?.data} />
-//   </Split>
-// }
-
 function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) {
 
   const connection = React.useContext(ConnectionContext)
@@ -564,18 +586,20 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
       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)
-      }
+      if (model) { // in case of broken pipe, this remains null
+        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(); }
+        return () => {
+          editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
+          model.dispose(); }
+      }
     }
   }, [editor, levelId, connection, leanClientStarted])
 
@@ -584,14 +608,16 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
     if (editor && leanClientStarted) {
 
       let model = monaco.editor.getModel(uri)
-      infoviewApi.serverRestarted(leanClient.initializeResult)
+      if (model) {
+        infoviewApi.serverRestarted(leanClient.initializeResult)
 
-      infoProvider.openPreview(editor, infoviewApi)
+        infoProvider.openPreview(editor, infoviewApi)
 
-      const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
-      const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
+        const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
+        const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
 
-      return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
+        return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
+      }
     }
   }, [editor, connection, leanClientStarted])
 
@@ -617,7 +643,7 @@ function useLoadWorldFiles(worldId) {
           models.push(monaco.editor.createModel(code, 'lean4', uri))
         }
       }
-      return () => { for (let model of models) { model.dispose() } }
+      return () => { for (let model of models) { try {model.dispose()} catch {console.log(`failed to dispose model ${model}`)}} }
     }
   }, [gameInfo.data, worldId])
 }

client/src/components/popup/erase.tsx

@@ -0,0 +1,59 @@
+/**
+ * @fileOverview
+*/
+import * as React from 'react'
+import { useSelector } from 'react-redux'
+import { GameIdContext } from '../../app'
+import { useAppDispatch } from '../../hooks'
+import { deleteProgress, selectProgress } from '../../state/progress'
+import { downloadFile } from '../world_tree'
+import { Button } from '../button'
+
+/** download the current progress (i.e. what's saved in the browser store) */
+export function downloadProgress(gameId: string, gameProgress: any, ev: React.MouseEvent) {
+  ev.preventDefault()
+  downloadFile({
+    data: JSON.stringify(gameProgress, null, 2),
+    fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
+    fileType: 'text/json',
+  })
+}
+
+/** Pop-up to delete game progress.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+export function ErasePopup ({handleClose}) {
+  const gameId = React.useContext(GameIdContext)
+  const gameProgress = useSelector(selectProgress(gameId))
+  const dispatch = useAppDispatch()
+
+  const eraseProgress = () => {
+    dispatch(deleteProgress({game: gameId}))
+    handleClose()
+  }
+
+  const downloadAndErase = (ev) => {
+    downloadProgress(gameId, gameProgress, ev)
+    eraseProgress()
+  }
+
+  return <div className="modal-wrapper">
+  <div className="modal-backdrop" onClick={handleClose} />
+  <div className="modal">
+    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
+    <h2>Delete Progress?</h2>
+
+    <p>Do you want to delete your saved progress irreversibly?</p>
+    <p>
+      (This deletes your proofs and your collected inventory.
+      Saves from other games are not deleted.)
+    </p>
+
+    <Button onClick={eraseProgress} to="">Delete</Button>
+    <Button onClick={downloadAndErase} to="">Download & Delete</Button>
+    <Button onClick={handleClose} to="">Cancel</Button>
+  </div>
+</div>
+}

client/src/components/popup/game_info.tsx

@@ -0,0 +1,23 @@
+/**
+ * @fileOverview
+*/
+import * as React from 'react'
+import { Typography } from '@mui/material'
+import Markdown from '../markdown'
+
+/** Pop-up that is displaying the Game Info.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+export function InfoPopup ({info, handleClose}: {info: string, handleClose: () => void}) {
+  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="welcome-text">
+      <Markdown>{info}</Markdown>
+    </Typography>
+  </div>
+</div>
+}

client/src/components/popup/privacy_policy.tsx

@@ -11,7 +11,7 @@ import * as React from 'react'
  * controlled by the containing element.
  */
 export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
-  return <div className="modal-wrapper">
+  return <div className="privacy-policy modal-wrapper">
   <div className="modal-backdrop" onClick={handleClose} />
   <div className="modal">
     <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
@@ -31,7 +31,7 @@ export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
     <p>Our server is located in Germany.</p>
     <p>
       <strong>Contact information:</strong><br />
-      Jon Eugster<br />
+      Alexander Bentkamp, Jon Eugster<br />
       Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
       Universitätsstr. 1<br />
       40225 Düsseldorf<br />
@@ -39,6 +39,21 @@ export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
       +49 211 81-12173<br />
       <a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Contact Details</a>
     </p>
+    <h2>Development &amp; Funding</h2>
+    <p>
+      The source code of this Lean game engine
+      is <a href="https://github.com/leanprover-community/lean4game" target="_blank">available on Github</a>.
+      If you experience any problems, please
+      file an <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">Issue on Github</a> or
+      get directly in contact.
+    </p>
+    <p>
+      The game engine has been developed as part of the
+      project <a href="https://hhu-adam.github.io/" target="_blank">ADAM: Anticipating the Digital
+      Age of Mathematics</a> at
+      Heinrich-Heine-Universität Düsseldorf. It is funded by
+      the <i>Stiftung Innovation in der Hochschullehre</i> as part of project <i>Freiraum 2022</i>.
+    </p>
   </div>
 </div>
 }
@@ -58,49 +73,3 @@ export const PrivacyPolicy: React.FC = () => {
     </>
   )
 }
-
-export function Impressum({handleClose}) {
-  return <div className="impressum">
-    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h2>Funding</h2>
-    <p>
-      This Lean game engine has been developed as part of the
-      project <a href="https://hhu-adam.github.io/" target="_blank">ADAM: Anticipating the Digital
-      Age of Mathematics</a> at
-      Heinrich-Heine-Universität Düsseldorf. It is funded by
-      the <i>Stiftung Innovation in der Hochschullehre</i> as part of project <i>Freiraum 2022</i>.
-    </p>
-
-    <h2>Development</h2>
-    <p>
-      The source code is <a href="https://github.com/leanprover-community/lean4game" target="_blank">available on Github</a>.
-      If you experience any problems, please
-      file an <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">Issue on Github</a> or
-      get directly in contact.
-    </p>
-    <h2>Privacy Policy &amp; Impressum</h2>
-    <p>
-      Our server collects metadata (such as IP address, browser, operating system)
-      and the data that the user enters into the editor. The data is used to
-      compute the Lean output and display it to the user. The information will be stored
-      as long as the user stays on our website and will be deleted immediately afterwards.
-      We keep logs to improve our software, but the contained data is anonymised.
-    </p>
-    <p>
-      We do not use cookies, but your game progress is stored in the browser storage
-      as site data. Your game progress is not saved on the server; if you delete
-      your browser storage, it is completely gone.
-    </p>
-    <p>Our server is located in Germany.</p>
-    <p>
-      <strong>Contact information:</strong><br />
-      Jon Eugster<br />
-      Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
-      Universitätsstr. 1<br />
-      40225 Düsseldorf<br />
-      Germany<br />
-      +49 211 81-12173<br />
-      <a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Contact Details</a>
-    </p>
-  </div>
-}

client/src/components/popup/rules_help.tsx

@@ -0,0 +1,55 @@
+/**
+ * @fileOverview
+*/
+import * as React from 'react'
+
+/** Pop-up that is displayed when opening the help explaining the game rules.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+export function RulesHelpPopup ({handleClose}: {handleClose: () => void}) {
+  return <div className="privacy-policy modal-wrapper">
+  <div className="modal-backdrop" onClick={handleClose} />
+  <div className="modal">
+    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
+    <h2>Game Rules</h2>
+    <p>
+      Game rules determine if it is allowed to skip levels and if the games runs checks to only
+      allow unlocked tactics and theorems in proofs.
+    </p>
+    <p>
+      Note: "Unlocked" tactics (or theorems) are determined by two things: The set of minimal
+      tactics needed to solve a level, plus any tactics you unlocked in another level. That means
+      if you unlock <code>simp</code> in a level, you can use it henceforth in any level.
+    </p>
+    <p>The options are:</p>
+    <table>
+      <thead>
+        <tr>
+          <th scope="col"></th>
+          <th scope="col">levels</th>
+          <th scope="col">tactics</th>
+        </tr>
+      </thead>
+      <tbody>
+        <tr>
+          <th scope="row">regular</th>
+          <td>🔐</td>
+          <td>🔐</td>
+        </tr>
+        <tr>
+          <th scope="row">relaxed</th>
+          <td>🔓</td>
+          <td>🔐</td>
+        </tr>
+        <tr>
+          <th scope="row">none</th>
+          <td>🔓</td>
+          <td>🔓</td>
+        </tr>
+      </tbody>
+    </table>
+  </div>
+</div>
+}

client/src/components/popup/upload.tsx

@@ -0,0 +1,70 @@
+/**
+ * @fileOverview
+*/
+import * as React from 'react'
+import { useSelector } from 'react-redux'
+import { GameIdContext } from '../../app'
+import { useAppDispatch } from '../../hooks'
+import { GameProgressState, loadProgress, selectProgress } from '../../state/progress'
+import { downloadFile } from '../world_tree'
+import { Button } from '../button'
+
+/** Pop-up that is displaying the Game Info.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+export function UploadPopup ({handleClose}) {
+  const [file, setFile] = React.useState<File>();
+  const gameId = React.useContext(GameIdContext)
+  const gameProgress = useSelector(selectProgress(gameId))
+  const dispatch = useAppDispatch()
+
+  const handleFileChange = (e) => {
+    if (e.target.files) {
+      setFile(e.target.files[0])
+    }
+  }
+
+  /** Upload progress from a  */
+  const uploadProgress = (e) => {
+    if (!file) {return}
+    const fileReader = new FileReader()
+    fileReader.readAsText(file, "UTF-8")
+    fileReader.onload = (e) => {
+      const data = JSON.parse(e.target.result.toString()) as GameProgressState
+      console.debug("Json Data", data)
+      dispatch(loadProgress({game: gameId, data: data}))
+    }
+    handleClose()
+  }
+
+  /** Download the current progress (i.e. what's saved in the browser store) */
+  const downloadProgress = (e) => {
+    e.preventDefault()
+    downloadFile({
+      data: JSON.stringify(gameProgress, null, 2),
+      fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
+      fileType: 'text/json',
+    })
+  }
+
+
+  return <div className="modal-wrapper">
+  <div className="modal-backdrop" onClick={handleClose} />
+  <div className="modal">
+    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
+    <h2>Upload Saved Progress</h2>
+
+    <p>Select a JSON file with the saved game progress to load your progress.</p>
+
+    <p><b>Warning:</b> This will delete your current game progress!
+      Consider <a className="download-link" onClick={downloadProgress} >downloading your current progress</a> first!</p>
+    <p>
+      <input type="file" onChange={handleFileChange}/>
+    </p>
+
+    <Button to="" onClick={uploadProgress}>Load selected file</Button>
+  </div>
+</div>
+}

client/src/components/welcome.tsx

@@ -1,29 +1,32 @@
 import * as React from 'react'
-import { useState, useEffect } from 'react'
-import { useSelector } from 'react-redux'
+import { useEffect } from 'react'
 import Split from 'react-split'
-import { Box, Typography, CircularProgress } from '@mui/material'
+import { Box, CircularProgress } from '@mui/material'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faGlobe, faBook, faArrowRight, faArrowLeft } from '@fortawesome/free-solid-svg-icons'
+import { faArrowRight } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
-import { useAppDispatch } from '../hooks'
-import { GameProgressState, changedOpenedIntro, deleteProgress, loadProgress, selectOpenedIntro, selectProgress } from '../state/progress'
+import { useAppDispatch, useAppSelector } from '../hooks'
+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 Markdown from './markdown'
-import {PrivacyPolicyPopup} from './privacy_policy'
-import { WorldTreePanel, downloadFile } from './world_tree'
+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 { WorldTreePanel } from './world_tree'
 
-import './welcome.css'
+import '../css/welcome.css'
 import { WelcomeAppBar } from './app_bar'
 import { Hint } from './hints'
 
-/** The panel showing the game's introduction text */
-function IntroductionPanel({introduction}: {introduction: string}) {
-  const {mobile, setPageNumber} = React.useContext(MobileContext)
+
+/** the panel showing the game's introduction text */
+function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) {
+  const {mobile} = React.useContext(MobileContext)
   const gameId = React.useContext(GameIdContext)
   const dispatch = useAppDispatch()
 
@@ -43,11 +46,6 @@ function IntroductionPanel({introduction}: {introduction: string}) {
         : <></>
       ))}
     </div>
-    {/* <Typography variant="body1" component="div" className="welcome-text">
-          <h1>{title}</h1>
-          <Markdown>{introduction}</Markdown>
-        </Typography>
-    */}
     {mobile &&
       <div className="button-row">
         <Button className="btn" to=""
@@ -62,142 +60,32 @@ function IntroductionPanel({introduction}: {introduction: string}) {
   </div>
 }
 
-export function InfoPopup ({info, handleClose}: {info: string, handleClose: () => void}) {
-  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="welcome-text">
-      <Markdown>{info}</Markdown>
-    </Typography>
-  </div>
-</div>
-}
-
-
-function ErasePopup ({handleClose}) {
-  const gameId = React.useContext(GameIdContext)
-  const gameProgress = useSelector(selectProgress(gameId))
-  const dispatch = useAppDispatch()
-
-  /** Download the current progress (i.e. what's saved in the browser store) */
-  const downloadProgress = (e) => {
-    e.preventDefault()
-    downloadFile({
-      data: JSON.stringify(gameProgress, null, 2),
-      fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
-      fileType: 'text/json',
-    })
-  }
-
-  const eraseProgress = () => {
-    dispatch(deleteProgress({game: gameId}))
-    handleClose()
-  }
-
-  const downloadAndErase = (e) => {
-    downloadProgress(e)
-    eraseProgress()
-  }
-
-  return <div className="modal-wrapper">
-  <div className="modal-backdrop" onClick={handleClose} />
-  <div className="modal">
-    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h2>Delete Progress?</h2>
-
-    <p>Do you want to delete your saved progress irreversibly?</p>
-    <p>
-      (This deletes your proofs and your collected inventory.
-      Saves from other games are not deleted.)
-    </p>
-
-    <Button onClick={eraseProgress} to="">Delete</Button>
-    <Button onClick={downloadAndErase} to="">Download & Delete</Button>
-    <Button onClick={handleClose} to="">Cancel</Button>
-  </div>
-</div>
-}
-
-function UploadPopup ({handleClose}) {
-  const [file, setFile] = React.useState<File>();
-  const gameId = React.useContext(GameIdContext)
-  const gameProgress = useSelector(selectProgress(gameId))
-  const dispatch = useAppDispatch()
-
-  const handleFileChange = (e) => {
-    if (e.target.files) {
-      setFile(e.target.files[0])
-    }
-  }
-
-  /** Upload progress from a  */
-  const uploadProgress = (e) => {
-    if (!file) {return}
-    const fileReader = new FileReader()
-    fileReader.readAsText(file, "UTF-8")
-    fileReader.onload = (e) => {
-      const data = JSON.parse(e.target.result.toString()) as GameProgressState
-      console.debug("Json Data", data)
-      dispatch(loadProgress({game: gameId, data: data}))
-    }
-    handleClose()
-  }
-
-  /** Download the current progress (i.e. what's saved in the browser store) */
-  const downloadProgress = (e) => {
-    e.preventDefault()
-    downloadFile({
-      data: JSON.stringify(gameProgress, null, 2),
-      fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
-      fileType: 'text/json',
-    })
-  }
-
-
-  return <div className="modal-wrapper">
-  <div className="modal-backdrop" onClick={handleClose} />
-  <div className="modal">
-    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h2>Upload Saved Progress</h2>
-
-    <p>Select a JSON file with the saved game progress to load your progress.</p>
-
-    <p><b>Warning:</b> This will delete your current game progress!
-      Consider <a className="download-link" onClick={downloadProgress} >downloading your current progress</a> first!</p>
-
-    <input type="file" onChange={handleFileChange}/>
-
-    <Button to="" onClick={uploadProgress}>Load selected file</Button>
-  </div>
-</div>
-}
-
-/** main page of the game showing amoung others the tree of worlds/levels */
+/** main page of the game showing among others the tree of worlds/levels */
 function Welcome() {
   const gameId = React.useContext(GameIdContext)
-  const {mobile, pageNumber, setPageNumber} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(MobileContext)
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
-  // impressum pop-up
+  // For mobile only
+  const openedIntro = useAppSelector(selectOpenedIntro(gameId))
+  const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0)
+
+  // pop-ups
+  const [eraseMenu, setEraseMenu] = React.useState(false)
   const [impressum, setImpressum] = React.useState(false)
-  function closeImpressum() {setImpressum(false)}
-  function toggleImpressum() {setImpressum(!impressum)}
-
   const [info, setInfo] = React.useState(false)
-  function closeInfo() {setInfo(false)}
-  function toggleInfo() {setInfo(!impressum)}
-
-
-  /* state variables to toggle the pop-up menus */
-  const [eraseMenu, setEraseMenu] = React.useState(false);
-  const openEraseMenu = () => setEraseMenu(true);
-  const closeEraseMenu = () => setEraseMenu(false);
-  const [uploadMenu, setUploadMenu] = React.useState(false);
-  const openUploadMenu = () => setUploadMenu(true);
-  const closeUploadMenu = () => setUploadMenu(false);
-
+  const [rulesHelp, setRulesHelp] = React.useState(false)
+  const [uploadMenu, setUploadMenu] = React.useState(false)
+  function closeEraseMenu()   {setEraseMenu(false)}
+  function closeImpressum()   {setImpressum(false)}
+  function closeInfo()        {setInfo(false)}
+  function closeRulesHelp()   {setRulesHelp(false)}
+  function closeUploadMenu()  {setUploadMenu(false)}
+  function toggleEraseMenu()  {setEraseMenu(!eraseMenu)}
+  function toggleImpressum()  {setImpressum(!impressum)}
+  function toggleInfo()       {setInfo(!info)}
+  function toggleUploadMenu() {setUploadMenu(!uploadMenu)}
 
   // set the window title
   useEffect(() => {
@@ -211,28 +99,32 @@ function Welcome() {
       <CircularProgress />
     </Box>
   : <>
-    <WelcomeAppBar gameInfo={gameInfo.data} toggleImpressum={toggleImpressum} openEraseMenu={openEraseMenu}
-      openUploadMenu={openUploadMenu} toggleInfo={toggleInfo} />
+    <WelcomeAppBar pageNumber={pageNumber} setPageNumber={setPageNumber} gameInfo={gameInfo.data} toggleImpressum={toggleImpressum}
+      toggleEraseMenu={toggleEraseMenu} toggleUploadMenu={toggleUploadMenu}
+      toggleInfo={toggleInfo} />
     <div className="app-content">
       { mobile ?
           <div className="welcome mobile">
             {(pageNumber == 0 ?
-              <IntroductionPanel introduction={gameInfo.data?.introduction} />
+              <IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
             : pageNumber == 1 ?
-              <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize} />
+              <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
+                rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
             :
               <InventoryPanel levelInfo={inventory?.data} />
             )}
           </div>
         :
           <Split className="welcome" minSize={0} snapOffset={200}  sizes={[25, 50, 25]}>
-            <IntroductionPanel introduction={gameInfo.data?.introduction} />
-            <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize} />
+            <IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
+            <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
+              rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
             <InventoryPanel levelInfo={inventory?.data} />
           </Split>
       }
     </div>
     {impressum ? <PrivacyPolicyPopup handleClose={closeImpressum} /> : null}
+    {rulesHelp ? <RulesHelpPopup handleClose={closeRulesHelp} /> : null}
     {eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
     {uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
     {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}

client/src/components/world_tree.tsx

@@ -8,16 +8,14 @@ import { Slider } from '@mui/material'
 import cytoscape, { LayoutOptions } from 'cytoscape'
 import klay from 'cytoscape-klay'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faDownload, faUpload, faEraser, faGlobe, faArrowLeft } from '@fortawesome/free-solid-svg-icons'
+import { faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
 import { useAppDispatch } from '../hooks'
-import { deleteProgress, selectProgress, loadProgress, GameProgressState,
-  selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
+import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
 import { store } from '../state/store'
-import { Button } from './button'
 
-import './world_tree.css'
+import '../css/world_tree.css'
 
 // Settings for the world tree
 cytoscape.use( klay )
@@ -28,8 +26,11 @@ const lineWidth = 10      //
 const ds = .75  // scale the resulting svg image
 
 const NMIN = 5   // min. worldsize
-const NLABEL = 9 // max. world size to display label below the world
+const NLABEL = 8 // max. world size to display label below the world
 const NMAX = 16  // max. world size. Level icons start spiraling out if the world has more levels.
+const NSPIRAL = 12 // world size if NMAX has been passed and need to spiral.
+
+const MINFONT = 12
 
 // colours
 const grey = '#999'
@@ -54,8 +55,9 @@ export function LevelIcon({ world, level, position, completed, unlocked, worldSi
 
   const N = Math.max(worldSize, NMIN)
 
-  // divide circle into `N+2` equal pieces
-  const beta = 2 * Math.PI / Math.min(N+2, (NMAX+1))
+  // divide circle into `N+2` equal pieces.
+  // only for non-spiraling case
+  const beta = 2 * Math.PI / Math.min(N+2, ((N < (NMAX+1) ? NMAX : NSPIRAL)+1))
 
   // We want distance between two level icons to be `2.2*r`, therefore:
   // Sinus-Satz: (1.1*r) / sin(β/2) = R / sin(π/2)
@@ -70,19 +72,19 @@ export function LevelIcon({ world, level, position, completed, unlocked, worldSi
    * works fine in tests up to `N=30`.
    */
   function betaSpiral(level) {
-    return 2 * Math.PI / ((NMAX+1) + Math.max(0, (level-2)) / (NMAX+1))
+    return 2 * Math.PI / ((NSPIRAL+1) + 2 * Math.max(0, (level-2)) / (NSPIRAL+1))
   }
 
   const x = N < (NMAX+1) ?
     // normal case
     s * position.x + Math.sin(level * beta) * R :
     // spiraling case
-    s * position.x + Math.sin(level * betaSpiral(level)) * (R + 2*r*(level-1)/(NMAX+1))
+    s * position.x + Math.sin(level * betaSpiral(level)) * (R + 2*r*(level-1)/(NSPIRAL+1))
   const y = N < (NMAX+1) ?
     // normal case
     s * position.y - Math.cos(level * beta) * R :
     // spiraling case
-    s * position.y - Math.cos(level * betaSpiral(level)) * (R + 2*r*(level-1)/(NMAX+1))
+    s * position.y - Math.cos(level * betaSpiral(level)) * (R + 2*r*(level-1)/(NSPIRAL+1))
 
   return (
     <Link to={levelDisabled ? '' : `/${gameId}/world/${world}/level/${level == 1 ? 0 : level}`}
@@ -112,9 +114,11 @@ export function WorldIcon({world, title, position, completedLevels, difficulty,
 
   // See level icons. Match radius computed there minus `1.2*r`
   const N = Math.max(worldSize, NMIN)
-  const betaHalf = Math.PI / Math.min(N+2, (NMAX + 1))
+  const betaHalf = Math.PI / Math.min(N+2, ((N < (NMAX+1) ? NMAX : NSPIRAL) + 1))
   let R = 1.1 * r / Math.sin(betaHalf) - 1.2 * r
 
+  let fontSize = Math.floor(R/4)
+
   // Offset for the labels for small worlds
   let labelOffset = R + 2.5 * r
 
@@ -137,12 +141,14 @@ export function WorldIcon({world, title, position, completedLevels, difficulty,
       className={playable ? '' : 'disabled'}>
     <circle className="world-circle" cx={s*position.x} cy={s*position.y} r={R}
         fill={completed ? green : unlocked ? blue : grey}/>
-    {worldSize > NLABEL ?
+    { false ? // fontSize >= MINFONT ?
+      // NOTE: This code would display the world names inside the bubble, but currently
+      //       it isn't used.
       // Label for large worlds
       <foreignObject className="world-title-wrapper" x={s*position.x} y={s*position.y}
           width={1.42*R} height={1.42*R} transform={"translate("+ -.71*R +","+ -.71*R +")"}>
         <div className={unlocked && !completed ? "playable-world" : ''}>
-          <p className="world-title" style={{fontSize: Math.floor(R/4) + "px"}}>
+          <p className="world-title" style={{fontSize: fontSize + "px"}}>
             {title ? title : world}
           </p>
         </div>
@@ -153,7 +159,7 @@ export function WorldIcon({world, title, position, completedLevels, difficulty,
           width='150px' height='2em' style={{overflow: 'visible'}}
           >
         <div className='world-label' style={{backgroundColor: completed ? darkgreen : unlocked ? darkblue : darkgrey}}>
-          <p className='world-title'>
+          <p className='world-title' style={{fontSize: MINFONT + "px"}}>
             {title ? title : world}
           </p>
         </div>
@@ -187,7 +193,7 @@ export const downloadFile = ({ data, fileName, fileType } :
 }
 
 /** The menu that is shown next to the world selection graph */
-export function WorldSelectionMenu() {
+export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
   const gameId = React.useContext(GameIdContext)
   const difficulty = useSelector(selectDifficulty(gameId))
   const dispatch = useAppDispatch()
@@ -196,12 +202,15 @@ export function WorldSelectionMenu() {
     return x == 0 ? 'none' : x == 1 ? 'relaxed' : 'regular'
   }
 
+
   return <nav className="world-selection-menu">
     <div className="slider-wrap">
-      <span className="difficulty-label">Game Rules</span>
+      <span className="difficulty-label">Rules
+        <FontAwesomeIcon icon={rulesHelp ? faXmark : faCircleQuestion} className='helpButton' onClick={() => (setRulesHelp(!rulesHelp))}/>
+      </span>
       <Slider
         orientation="vertical"
-        title="Game Rules:&#10;- regular: 🔐 levels, 🔐 tactics&#10;- relaxed: 🔓 levels, 🔐 tactics&#10;- none: 🔓 levels, 🔓 tactics"
+        title="Game Rules"
         min={0} max={2}
         aria-label="Game Rules"
         defaultValue={difficulty}
@@ -256,9 +265,12 @@ export function computeWorldLayout(worlds) {
 }
 
 
-export function WorldTreePanel({worlds, worldSize}:
+export function WorldTreePanel({worlds, worldSize, rulesHelp, setRulesHelp}:
   { worlds: any,
-    worldSize: any}) {
+    worldSize: any,
+    rulesHelp: boolean,
+    setRulesHelp: any,
+  }) {
   const gameId = React.useContext(GameIdContext)
   const difficulty = useSelector(selectDifficulty(gameId))
   const {nodes, bounds}: any = worlds ? computeWorldLayout(worlds) : {nodes: []}
@@ -342,7 +354,7 @@ export function WorldTreePanel({worlds, worldSize}:
   let dx = bounds ? s*(bounds.x2 - bounds.x1) + 2*padding : null
 
   return <div className="column">
-      <WorldSelectionMenu />
+      <WorldSelectionMenu rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
       <svg xmlns="http://www.w3.org/2000/svg" xmlnsXlink="http://www.w3.org/1999/xlink"
           width={bounds ? `${ds * dx}` : ''}
           viewBox={bounds ? `${s*bounds.x1 - padding} ${s*bounds.y1 - padding} ${dx} ${s*(bounds.y2 - bounds.y1) + 2 * padding}` : ''}

client/src/css/app.css

@@ -108,6 +108,7 @@ em {
   flex: 0;
   background: var(--clr-primary);
   display: flex;
+  position: relative;
   flex-direction: row;
   justify-content: space-between;
   padding: 1.1em;
@@ -139,3 +140,7 @@ em {
 .markdown ul, .markdown ol {
 	margin:0 1.5em 1.5em 1.5em;
 }
+
+.privacy-policy {
+  z-index: 10;
+}

client/src/css/infoview.css

@@ -43,7 +43,7 @@
   font-weight: 500;
 }
 
-.command-line {
+.typewriter {
   background: var(--clr-primary);
   padding: 0.5em;
   font-family: var(--ff-primary);
@@ -51,17 +51,33 @@
   /* margin: 0.2em 0 0; */
 }
 
-.command-line form {
+.typewriter.disabled{
+  background: #bbb;
+}
+
+.typewriter.disabled .btn-inverted,
+.typewriter.disabled .mtk1 {
+  color: #777;
+}
+
+.typewriter.disabled .typewriter-input-wrapper,
+.typewriter.disabled .monaco-editor,
+.typewriter.disabled .monaco-editor-background,
+.typewriter.disabled .btn-inverted {
+  background-color: #eee;
+}
+
+.typewriter form {
   display: flex;
 }
 
-.command-line button, .undo-button {
+.typewriter button, .undo-button {
   display: block;
   white-space: nowrap;
   flex: 0;
 }
 
-.command-line .command-line-input-wrapper{
+.typewriter .typewriter-input-wrapper{
   min-width: 0;
   flex: 1;
   padding: 0.4em .6em 0;
@@ -71,15 +87,22 @@
   flex-direction: column;
 }
 
-.command-line .command-line-input {
+.typewriter-interface .proof .MuiCircularProgress-root {
+  left: 50%;
+  position: relative;
+  margin-left: -20px;
+  margin-bottom: 0.6em;
+}
+
+.typewriter .typewriter-input {
   flex: 1;
 }
 
 /* Turn off some monaco decorations: */
-.command-line-input .monaco-editor .view-overlays .current-line {
+.typewriter-input .monaco-editor .view-overlays .current-line {
   border: 0;
 }
-.command-line-input .monaco-editor .scroll-decoration {
+.typewriter-input .monaco-editor .scroll-decoration {
   box-shadow: none;
 }
 
@@ -138,7 +161,7 @@
 
 
 /* Push the goals to the bottom for now, until we insert the proof history above. */
-.commandline-interface .content {
+.typewriter-interface .content {
   display: flex;
   flex-direction: column;
   scroll-behavior: smooth;
@@ -149,7 +172,7 @@
   scroll-behavior: smooth;
 }
 
-.commandline-interface .content .tmp-pusher {
+.typewriter-interface .content .tmp-pusher {
   flex: 1;
 }
 
@@ -157,7 +180,10 @@
   background-color: #bbb;
   padding: .5em;
   border-radius: .2em;
-  margin-bottom: 2rem;
+  /* TODO: It seems my browsers merge the margings of the proof steps,
+  so that it only shows once 0.5rem instead of twice. Thus have 1.5 here now.
+  */
+  margin-bottom: 1.5rem;
   display: flex;
   flex-direction: row;
 }

client/src/css/level.css

@@ -41,6 +41,20 @@
   padding-right: .5em;
 }
 
+.exercise-statement {
+  padding-top: 1em;
+  padding-bottom: 1em;
+}
+
+.exercise-statement p {
+  margin: 0;
+}
+
+.exercise-statement .lean-code {
+  color: rgba(0, 32, 90, 0.87);
+  font-size: 12px; /* TODO: is the monaco font-size hardcoded? */
+}
+
 .conclusion {
   padding: 1em;
 }
@@ -218,17 +232,17 @@ td code  {
   height: 100%;
 } */
 
-.commandline-interface {
+.typewriter-interface {
   display: flex;
   flex-flow: column;
   height: 100%;
 }
 
-.command-line {
+.typewriter {
   flex: 0 1 auto;
 }
 
-.commandline-interface .content {
+.typewriter-interface .content {
   flex: 1 1 auto;
   overflow-y: scroll;
   padding: 0;
@@ -257,7 +271,7 @@ td code  {
   box-shadow: .0em .0em .4em .1em #8cbbe9;
 }
 
-.exercise .step.selected, .chat .selected {
+.exercise .step.selected .goal-tabs, .chat .selected {
   /* border: 3px solid #5191d1; */
   box-shadow: .0em .0em .4em .1em var(--clr-primary);
 }
@@ -318,11 +332,11 @@ td code  {
   justify-content: center;
 }
 
-.commandline-interface .content, .world-image-container.empty {
+.typewriter-interface .content, .world-image-container.empty {
   background-color: #eee;
 }
 
-.commandline-interface .proof {
+.typewriter-interface .proof {
   background-color: #fff;
 }
 

client/src/css/world_tree.css

@@ -49,7 +49,6 @@ svg .disabled {
 }
 
 .world-selection-menu {
-  padding: .5em 1em;
   position: absolute;
   right: 1em;
   top: 1em;
@@ -75,7 +74,7 @@ svg .disabled {
   /* width: 100%; */
   height: 7em;
   /* min-width: 16em; */
-  padding-bottom: .8em;
+  padding: .5em 1em 1.3em 1em;
   margin-left: auto;
   margin-right: auto;
 }
@@ -109,3 +108,10 @@ svg .disabled {
   padding: .2em;
   border-radius: .5em;
 }
+
+.world-selection-menu .helpButton {
+  position: absolute;
+  right: .5em;
+  top: .5em;
+  color: var(--clr-primary);
+}

client/src/state/api.ts

@@ -36,6 +36,7 @@ export interface LevelInfo {
   descrFormat: null|string,
   lemmaTab: null|string,
   statementName: null|string,
+  displayName: null|string,
   template: null|string
 }
 

doc/DOCUMENTATION.md

@@ -8,9 +8,7 @@ A game consist of worlds which have multiple levels each. In the following we de
 
 ### Level
 
-#### Preample
-
-A level file is a lean file that imports at least `GameServer.Commands` and starts with the four lean commands
+A level file is a lean file that imports at least `import GameServer.Commands` and starts with the following Lean commands.
 
 ```lean
 Game "NNG"
@@ -19,12 +17,12 @@ Level 1
 Title "The rfl tactic"
 ```
 
-Note that the levels inside a world must have consequtive numbering starting with `1`. The `Game`
-and `World` strings can be anything.
+Note that the levels inside a world must have consecutive numbering starting with `1`. The `Game`
+and `World` strings can be anything, see below.
 
 #### Statement
 
-The core of a level is the `Statement`, which is the exercise that should be proven:
+The core of a level is the `Statement`, which is the exercise that should be proven.
 
 ```lean
 /-- For all natural numbers $n$, we have $0 + n = n$. -/
@@ -53,10 +51,12 @@ There are a few extra tactics that help you structuring the proof:
 
 - `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches
   the one where `Hint` is placed. For more options about hints, see below.
-- `Branch`: In the proof you can add a `Branch` that runs an alternativ tactic sequence, which
+- `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which
   helps setting `Hints` in different   places. The `Branch` does not affect the main
   proof and does not need to finish any goals.
-- `Template`/`Hole`: not implemented yet, but used to provide a sample proof template.
+- `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template`
+  will be copied into the editor with all `Hole`s replaced with `sorry`. Note that
+  having a `Template` will force the user to use Editor-mode for this level.
 
 ##### Statement Name (optional)
 
@@ -77,26 +77,27 @@ There are three places where the documentation comment appears:
   description there including examples etc.
 
 Both latter points support Markdown (including katex).
+
 ##### Attributes (optional)
 
 the `@[ attributes ]` prefix should work just like you know it from the `theorem` keyword.
 
 #### Introduction/Conclusion
 
-Optionally, you can add a `Introduction "some text"` and `Conclusion "some text"` to your level.
+Optionally, you can add an `Introduction "some text"` and `Conclusion "some text"` to your level.
 The introduction will be shown at the beginning, the conclusion is displayed once the level
 is solved.
 
-#### Lemmas/Tactics/Definitions
+#### Theorems/Tactics/Definitions
 
-Only enabled lemmas/tactics/definitions (called "items" here) are available in a level.
+Only enabled theorems/tactics/definitions (called "items" here) are available in a level.
 
 To add a new item in a level, you can add
 
 ```lean
 NewTactic rfl simp
-NewLemma MyNat.add_zero
-NewDefinition Nat
+NewLemma MyNat.add_zero MyNat.add_succ
+NewDefinition Nat Pow Mul
 ```
 
 Once added, items will be available in all future levels/worlds,
@@ -107,7 +108,7 @@ DisabledTactic tauto
 DisabledLemma MyNat.add_zero
 ```
 
-or specify explicitely which items should be available with
+or specify explicitly which items should be available with
 
 ```lean
 OnlyTactic rw rfl apply
@@ -134,10 +135,9 @@ Introduction "some text"
 ```
 
 The `Title` is the world's display title. The `Introduction` is displayed before loading level 1.
-Note that all levels of a world should be imported by the world file and they **must not** be
-imported in another world's levels. (bug?)
+Note that all levels of a world should be imported by the world file.
 
-However, you can import an entire world in a different world's level: `import NNG.Levels.Addition`
+BUG: A level **must not** be imported in a different world's level. Instead, you have to import an entire world there: `import NNG.Levels.Addition`
 
 ### Game
 
@@ -152,17 +152,18 @@ Game "NNG"
 Title "Natural Number Game"
 Introduction "some text"
 
-Path Addition → Multiplication → Power
-
 MakeGame
 ```
 
-There can be several `Path` statements to define the relation between the worlds. The worlds
-must form a directed acyclic graph, i.e. have no loops. The order of worlds influences which tactics and lemmas will be unlocked in a given level.
+The game will automatically compute the order of the worlds depending on the sample proofs of the Levels (ignoring anything inside a `Branch`). You can add additional dependencies manually by adding `Dependency PowerWorld → ImpossibleWorld` before `MakeGame`.
+The order of worlds influences which tactics and lemmas will be unlocked in a given level.
+
+`MakeGame` will display warnings about things in the game that need to be fixed, like missing
+documentation or if a tactic is never introduced.
 
 ### Documentation
 
-Each tactic, lemma, or definition (all called items here) that is introduced in the game
+Each tactic, theorem, or definition (all called items here) that is introduced in the game
 needs a documentation entry. These are statements of the following form:
 
 ```lean
@@ -194,7 +195,7 @@ There will be features added to get automatic information from mathlib!
 
 Inside the doc comment you don't need to escape the backslashes:
 
-```
+```lean
 /-- $\operatorname{succ}(n)$. notation for naturals is `\N`. -/
 Statement ...
 ```
@@ -203,11 +204,17 @@ However, inside interpolated strings (e.g. in `Hint`, `Introduction` and `Conclu
 you do need to escape backslashes
 with `\\` and `{` with `\{`:
 
-```
+```lean
 Hint "This code has some $\\operatorname\{succ}(n)$ math. The value of `h` is {h}.
 Notation for naturals is `\\N`."
 ```
 
+## Game design
+Here are some things you should consider designing a new game:
+
+* A world with more than 16 levels will be displayed with the levels spiraling outwards,
+  it might be desirable to stay below that bound. Above 22 levels the spiral start getting out
+  of control.
 
 # Running Games Locally
 
@@ -217,7 +224,7 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w
 
 1.  **Install Docker and Dev Containers** *(once)*:<br/>
     See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
-    Explicitely this means:
+    Explicitly this means:
     * Install docker engine if you have not yet: [Instructions](https://docs.docker.com/engine/install/).
       I followed the "Server" instructions for linux.
     * Note that on Linux you need to add your user to the `docker` group
@@ -244,29 +251,30 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w
   running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
 * If the starting the container fails, in particular with a message `Error: network xyz not found`,
   you might have deleted stuff from docker via your shell. Try deleting the container and image
-  explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
+  explicitly in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
   container. (this will again take some time)
 
 
 ## Without Dev Containers
 Install `nvm`:
-```
+```bash
 curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
 ```
 then reopen bash and test with `command -v nvm` if it is available (Should print "nvm").
 
 Now install node:
-```
+```bash
 nvm install node
 ```
 
 Clone the game (e.g. `NNG4` here):
-```
-git clone git@github.com:hhu-adam/NNG4.git
+```bash
+git clone https://github.com/hhu-adam/NNG4.git
+# or: git clone git@github.com:hhu-adam/NNG4.git
 ```
 
 Download dependencies and build the game:
-```
+```bash
 cd NNG4
 lake update
 lake exe cache get   # if your game depends on mathlib
@@ -274,21 +282,22 @@ lake build
 ```
 
 Clone the game repository into a directory next to the game:
-```
+```bash
 cd ..
-git clone git@github.com:leanprover-community/lean4game.git
+git clone https://github.com/leanprover-community/lean4game.git
+# or: git clone git@github.com:leanprover-community/lean4game.git
 ```
 The folders `NNG4` and `lean4game` must be in the same directory!
 
 In `lean4game`, install dependencies:
-```
+```bash
 cd lean4game
 npm install
 ```
 
 If you are developing a game other than `Robo` or `NNG4`, adapt the
 code at the beginning of `lean4game/server/index.mjs`:
-```
+```typescript
 const games = {
     "g/hhu-adam/robo": {
         dir: "../../../../Robo",
@@ -302,7 +311,7 @@ const games = {
 ```
 
 Run the game:
-```
+```bash
 npm start
 ```
 
@@ -314,7 +323,7 @@ and the game is available on http://localhost:3000/#/g/hhu-adam/NNG4.
 When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with this
 setup by setting `export NODE_ENV=development` inside your local game before building it:
 
-```
+```bash
 cd NNG4
 export NODE_ENV=development
 lake update

doc/create_game.md

@@ -0,0 +1,255 @@
+# Creating a new game
+
+This tutorial walks you through creating a new game for lean4. It covers from writing new levels, over testing the game locally, to publishing the game online.
+
+## 1. Create the project
+
+1. Use the [NNG template](https://github.com/hhu-adam/NNG4) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
+2. Clone the game repo.
+3. Call `lake update && lake exe cache get && lake build` to build the Lean project.
+
+Note that you need to host your game's code on github to publish it online later on. If you only
+want to play it locally, you can simply clone the NNG repo and start modifying that one.
+
+
+## 2. Game.lean
+
+The file `Game.lean` is the backbone of the game putting everything together.
+
+1. `MakeGame`: This command is where the game gets built. If there are things to fix, they will be shown here as warnings or errors (orange/red squigglies in VSCode). Note that you might have to call "Lean: Restart File" (Ctrl+Shift+X) to reload the file and see changes made in other files.
+1. `Title`: Set the display title of your game.
+1. `Introduction`: This is the text displayed at the beginning next to the world selection tree.
+1. `Info`: This will be displayed in the game's menu as "Game Info". Use it for credits, funding and other meta information about the game.
+1. Imports: The file needs to import all world files, which we look at in a second. If you add a new world, remember to import it here!
+1. `Dependency`: (optional) This command adds another edge in the world tree. The game computes them automatically based on used tactics/theorems. However, sometimes you need a dependency the game can't compute, for example you explained `≠` in one world and in another world, the user is expected to know it already. The syntax is `Dependency World₁ → World₂ → World₃`.
+
+So the `Game.lean` has the following structure:
+
+```lean
+import GameServer.Commands
+
+-- import all worlds
+import Game.Levels.Tutorial
+
+Title "My Game"
+
+Introduction "
+Hi, nice you're here! Click on a world to start.
+"
+
+Info "
+This game has been developed by me.
+"
+
+-- Dependency World₁ → World₂ -- because of `≠`
+
+MakeGame
+```
+
+## 3. Creating a Level
+
+In this tutorial we first learn about Levels. A game consists of a tree of worlds, each world has
+a number of levels, enumerated 1 to n. Here we create level 1 of a world `MyWorld`. We add this world to the game in the next section.
+
+A minimal level file looks like the following. There are many options to add, which we will dive
+into in a later section
+
+```lean
+import GameServer.Commands
+
+World "MyWorld"
+Level 1
+Title "Hello World"
+
+Introduction "
+A message shown at the beginning of the level. Use it to explain any new concepts.
+"
+
+/-- The exercise statement in natural language using latex: $\iff$. -/
+Statement (n : Nat) : 0 + n = n := by
+  sorry
+
+Conclusion "
+The message shown when the level is completed
+"
+```
+
+1. Create a folder `Game/Levels/MyWorld`
+1. Create a file `Game/Levels/MyWorld/L01_hello.lean`
+1. Copy the above inside your first level.
+
+## 4. Creating a World
+
+Now we create a world. For that we create a file `MyWorld.lean` that imports all levels of this world:
+
+```lean
+import Game.Levels.MyWorld.L01_hello
+
+World "MyWorld"
+Title "My First World"
+
+Introduction
+"
+This introduction text is shown when one first enters a world.
+"
+```
+
+1. Create a file `Game/Levels/MyWorld.lean`
+1. Use the template above and make sure you import all levels of this world.
+1. In `Game.lean` import the world with `import Game.Levels.MyWorld`
+
+Now you created a world with one level and added it🎉 The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently it shows
+
+```text
+No world introducing sorry, but required by MyWorld
+```
+
+which means that the world `MyWorld` uses the tactic `sorry` in a proof, but `sorry` has not been
+introduced anywhere.
+
+## 5. Testing the Game Locally
+
+Now it's time to test the game locally and play it.
+
+There are multiple ways how you can start the game locally to test-play it described at [How to Run the Game Locally](running_locally.md). If you have problems getting one of the setups to work, please get in contact!
+
+
+## 6. Dive into Level creation
+
+Now that you have a running game, we have a closer look at the level files and all the options
+you have to design your game.
+
+### 6. a) Inventory
+
+The player has an inventory with tactics, theorems, and definitions that unlock during the game. You can unlock/introduce such items in a Level by adding one of the following below the `Statement`.
+
+```lean
+NewTactic induction simp
+NewLemma Nat.zero_mul
+NewDefinition Pow
+```
+
+#### Doc entries
+
+You'll see a warning about a missing Lemma documentation. You can fix it by adding doc-entries like the following somewhere above it.
+
+```lean
+LemmaDoc Nat.zero_mul as "zero_mul" in "Mul"
+"some description"
+
+TacticDoc simp
+"some description"
+
+DefinitionDoc Pow as "^"
+"some description"
+```
+
+(e.g. you could also create a file `Game/Doc/MyTheorems.lean`, add there your documentation and import it)
+
+If you do not provide any content for the inventory, the game will try to find a docstring of that item and display that docstring.
+
+#### Inventory management
+
+You have a few options to disable inventory items that have been unlocked in previous levels:
+
+```lean
+DisableTactic, DisableLemma, OnlyTactic, OnlyLemma
+```
+
+have the same syntax as above. The former two disable items for this level, the latter two
+disable all items except the ones specified.
+
+#### Theorem Tab
+
+Theorems are sorted into tabs. with `LemmaTab "Mul"` you specify which tab should be open by default in this level.
+
+#### HiddenTactic
+
+`NewHiddenTactic` lets you add a tactic without adding it to the inventory. This can be useful for variants of tactics. E.g. you could do
+
+```lean
+NewTactic rw
+NewHiddenTactic rewrite nth_rewrite rwa
+```
+
+and only `rw` would show up in the inventory.
+
+### 6. b) Statement
+
+The statement is the exercise of the level. the basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax
+
+#### Name
+
+You can give your exercise a name: `Statement my_first_exercise (n : Nat) ...`. If you do so, it will be added to the inventory and be available in future levels.
+
+#### Doc String / Exercise statement
+
+Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports Latex.
+
+```lean
+/-- The exercise statement in natural language using latex: $\iff$. -/
+Statement ...
+  sorry
+```
+
+#### Attributes
+
+You can add attributes as you would for a `theorem`. Most notably, you can make your named exercise a `simp` lemma:
+
+```lean
+@[simp]
+Statement my_simp_lemma ...
+```
+
+### 6. c) Proof
+
+The proof must always be a tactic proof, i.e. `:= by` is a mandatory part of the syntax.
+
+There are a few extra tactics that help you structuring the proof:
+
+- `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches
+  the one where `Hint` is placed. For more options about hints, see below.
+- `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which
+  helps setting `Hints` in different places. The `Branch` does not affect the main
+  proof and does not need to finish any goals.
+- `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template`
+  will be copied into the editor with all `Hole`s replaced with `sorry`. Note that
+  having a `Template` will force the user to use Editor-mode for this level.
+
+One thing to keep in mind is that the game will look at the main proof to figure out which tactics and theorems are needed, but it ignores any `Branch`es.
+
+### 6. d) Hints
+
+Most important for game development are probably the `Hints`.
+
+The hints will be displayed whenever the player's current goal matches the goal the hint is
+placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands. If you specify
+
+```
+Hint (strict := true) "some hidden hint"
+```
+
+a hint only matches iff the assumptions match exactly one-to-one. (Otherwise, it does not care if there are additional assumptions in context)
+
+Further, you can choose to hide hints and only have them displayed when the player presses "More Help":
+```
+Hint (hidden := true) "some hidden hint"
+```
+
+Lastly, you should put variable names in hints inside brackets:
+
+```
+Hint "now use `rw [{h}]` to use your assumption {h}."
+```
+That way, the game will replace it with the actual name the assumption has in the player's proof state.
+
+## Further Notes
+
+Here are some random further things you should consider designing a new game:
+
+* Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you
+  would write `Introduction "some latex here: $\\iff$."` but
+  `/-- some latex here: $\iff$. -/ Statement ...`
+* A world with more than 16 levels will be displayed with the levels spiraling outwards,
+  it might be desirable to stay below that bound. Above 22 levels the spiral starts getting out
+  of control.

doc/npm_scripts.md

@@ -0,0 +1,9 @@
+## NPM Scripts
+
+* `npm start`: Start the project in development mode. The browser will automatically reload when client files get changed. The Lean server will get recompiled and restarted when lean files get changed. The Lean server will be started without a container. The client and server can be started separately using the scripts `npm run start_client` and `npm run start_server`. The project can be accessed via `http://localhost:3000`.
+Internally, websocket requests to `ws://localhost:3000/websockets` will be forwarded to a Lean server running on port `8080`.
+
+* `npm run build`: Build the project in production mode. All assets of the client will be compiled into `client/dist`.
+On the server side, the command will set up a docker image containing the Lean server. The two parts can be built separately using `npm run build_client` and `npm run build_server`.
+
+* `npm run production`: Start the project in production mode. This requires that the build script has been run. It will start a server on the port specified in the `PORT` environment variable or by default on `8080`. You can run on a specific port by running `PORT=80 npm run production`. The server will serve the files in `client/dist` via http and give access to the bubblewrapped Lean server via the web socket protocol.

doc/running_locally.md

@@ -0,0 +1,121 @@
+# Running Games Locally
+
+The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
+
+There are several options to play a game locally:
+
+- VSCode Dev Container: needs `docker` installed on your machine
+- Codespaces: Needs active internet connection and computing time is limited.
+- Gitpod: does not work yet (I that true?)
+- Manual installation: Needs `npm` installed on your system
+
+The recommended option is "VSCode Dev containers" but you may choose any option above depending on your setup.
+
+## VSCode Dev Containers
+
+1.  **Install Docker and Dev Containers** *(once)*:<br/>
+    See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
+    Explicitly this means:
+    * Install docker engine if you have not yet: [Instructions](https://docs.docker.com/engine/install/).
+      I followed the "Server" instructions for linux.
+    * Note that on Linux you need to add your user to the `docker` group
+      ([see instructions](https://docs.docker.com/engine/install/linux-postinstall/)) and probably reboot.
+    * Open the games folder in VSCode: `cd NNG4 && code .` or "Open Folder" within VSCode
+    * a message appears prompting you to install the "Dev Containers" extension (by Microsoft). (Alternatively install it from the VSCode extensions).
+
+2.  **Open Project in Dev Container** *(everytime)*:<br/>
+    Once you have the Dev Containers Extension installed, (re)open the project folder of your game in VSCode.
+    A message appears asking you to "Reopen in Container".
+
+    * The first start will take a while, ca. 2-10 minutes. After the first
+      start this should be very quickly.
+    * Once built, you can open http://localhost:3000 in your browser. which should load the game
+
+3.  **Editing Files** *(everytime)*:<br/>
+    After editing some Lean files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes.
+
+### Errors
+
+* If you don't get the pop-up, you might have disabled them and you can reenable it by
+  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
+* If the starting the container fails, in particular with a message `Error: network xyz not found`,
+  you might have deleted stuff from docker via your shell. Try deleting the container and image
+  explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
+  container. (this will again take some time)
+
+## Codespaces
+
+You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".
+
+Note: You have to wait until npm started properly. In particular, this is after a message like `[client] webpack 5.81.0 compiled successfully in 38119 ms` appears in the terminal, which might take a good while.
+
+As with devcontainers, you need to run `lake build` after changing any lean files and then reload the browser.
+
+## Gitpod
+
+TODO: Not sure this works yet!
+
+Open the game clicking on the gitpod link. Again you will need to wait until it is fully built and then enter `lake build` in the shell whenever you made changes.
+
+## Manual installation
+
+This installs the `lean4game` manually on your computer. (It is the same installation as one would
+use to setup a proper server online, only the run command (i.e. `npm start`) is different.)
+
+Install `nvm`:
+```bash
+curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
+```
+then reopen bash and test with `command -v nvm` if it is available (Should print "nvm").
+
+Now install node:
+```bash
+nvm install node
+```
+
+Clone the game (e.g. `NNG4` here):
+```bash
+git clone https://github.com/hhu-adam/NNG4.git
+# or: git clone git@github.com:hhu-adam/NNG4.git
+```
+
+Download dependencies and build the game:
+```bash
+cd NNG4
+lake update
+lake exe cache get   # if your game depends on mathlib
+lake build
+```
+
+Clone the game repository into a directory next to the game:
+```bash
+cd ..
+git clone https://github.com/leanprover-community/lean4game.git
+# or: git clone git@github.com:leanprover-community/lean4game.git
+```
+The folders `NNG4` and `lean4game` must be in the same directory!
+
+In `lean4game`, install dependencies:
+```bash
+cd lean4game
+npm install
+```
+
+Run the game:
+```bash
+npm start
+```
+
+This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/NNG4. Replace `NNG4` with the folder name of your local game.
+
+## Modifying the GameServer
+
+When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by setting `export NODE_ENV=development` inside your local game before building it:
+
+```bash
+cd NNG4
+export NODE_ENV=development
+lake update
+lake build
+```
+This causes lake to search locally for the `GameServer` lake package instead of using the version from github. Therefore, when you `lake build` your game, it will rebuild with the modified `GameServer`.

package.json

@@ -4,6 +4,7 @@
   "private": true,
   "homepage": ".",
   "dependencies": {
+    "@babel/plugin-transform-optional-chaining": "^7.23.0",
     "@emotion/react": "^11.10.5",
     "@emotion/styled": "^11.10.5",
     "@fontsource/roboto": "^4.5.8",

server/GameServer/AbstractCtx.lean

@@ -1,4 +1,5 @@
 import Lean
+import GameServer.Utils
 
 section AbstractCtx
 open Lean

server/GameServer/Commands.lean

@@ -10,6 +10,14 @@ register_option lean4game.showDependencyReasons : Bool := {
   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"` -/
@@ -72,6 +80,64 @@ 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.
@@ -94,13 +160,22 @@ def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.g
     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 "" })
-      logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
-        m!"somewhere above this statement.")
+        category := if type == .Lemma then s!"{n.getPrefix}" else ""
+        content := docstring})
     -- Add the default documentation
     | some s =>
       modifyEnv (inventoryTemplateExt.addEntry · {
@@ -109,8 +184,8 @@ def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.g
         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.")
+        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:
 
@@ -140,7 +215,7 @@ LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 * 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 requries
+Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
 The lemma/definition to have the same fully qualified name as in mathlib.
  -/
 elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
@@ -168,7 +243,7 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur
 * The string following `as` is the displayed name (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 requries
+Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
 The lemma/definition to have the same fully qualified name as in mathlib.
  -/
 elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
@@ -180,31 +255,17 @@ elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
 
 /-! ## Add inventory items -/
 
--- namespace Lean.PrettyPrinter
--- def ppSignature' (c : Name) : MetaM String := do
---   let decl ← getConstInfo c
---   let e := .const c (decl.levelParams.map mkLevelParam)
---   let (stx, _) ← delabCore e (delab := Delaborator.delabConstWithSignature)
---   let f ← ppTerm stx
---   return toString f
--- end Lean.PrettyPrinter
-
 def getStatement (name : Name) : CommandElabM MessageData := do
-  -- let c := name.getId
-
-  let decl ← getConstInfo name
-  -- -- TODO: How to go between CommandElabM and MetaM
-
-  -- addCompletionInfo <| .id name c (danglingDot := false) {} none
   return ← addMessageContextPartial (.ofPPFormat { pp := fun
-    | some ctx => ctx.runMetaM <| ppExpr decl.type
-    -- PrettyPrinter.ppSignature' c
-    -- PrettyPrinter.ppSignature c
+    | 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`. -/
+/-- 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
@@ -214,12 +275,15 @@ def getStatementString (name : Name) : CommandElabM String := do
 
 /-- Declare tactics that are introduced by this level. -/
 elab "NewTactic" args:ident* : command => do
-  for name in ↑args do checkInventoryDoc .Tactic name -- TODO: Add (template := "[docstring]")
+  for name in ↑args do
+    checkInventoryDoc .Tactic name -- TODO: Add (template := "[docstring]")
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with new := level.tactics.new ++ args.map (·.getId)}}
 
-/-- Declare tactics that are introduced by this level. -/
+/-- Declare tactics that are introduced by this level but do not show up in inventory. -/
 elab "NewHiddenTactic" args:ident* : command => do
+  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)}}
@@ -227,6 +291,8 @@ elab "NewHiddenTactic" args:ident* : command => do
 /-- 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}'."
     checkInventoryDoc .Lemma name -- TODO: Add (template := "[mathlib]")
   modifyCurLevel fun level => pure {level with
     lemmas := {level.lemmas with new := args.map (·.getId)}}
@@ -409,13 +475,11 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
   -- the namespace?
   let currNamespace ← getCurrNamespace
 
-  let st ← match statementName with
-  | some name => getStatementString <| currNamespace ++ name.getId
-  | none =>  getStatementString <| currNamespace ++ (defaultDeclName).getId
-
-  let head := match statementName with
-  | some name => Format.join ["theorem ", (currNamespace ++ name.getId).toString]
-  | none => "example"
+  -- Format theorem statement for displaying
+  let sigString := sig.raw.reprint.getD ""
+  let descrFormat : String := match statementName with
+  | some name =>  s!"theorem {name.getId} {sigString} := by"
+  | none => s!"example {sigString} := by"
 
   modifyCurLevel fun level => pure { level with
     module := env.header.mainModule
@@ -425,7 +489,7 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
     statementName := match statementName with
     | none => default
     | some name => currNamespace ++ name.getId
-    descrFormat := (Format.join [head, " ", st, " := by"]).pretty 10
+    descrFormat := descrFormat
     hints := hints
     tactics := {level.tactics with used := usedInventory.tactics.toArray}
     definitions := {level.definitions with used := usedInventory.definitions.toArray}
@@ -457,7 +521,7 @@ elab (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(t
   let mut strict := false
   let mut hidden := false
 
-  -- remove spaces at the beginngng of new lines
+  -- remove spaces at the beginning of new lines
   let msg := TSyntax.mk $ msg.raw.setArgs $ ← msg.raw.getArgs.mapM fun m => do
     match m with
     | Syntax.node info k args =>
@@ -511,9 +575,9 @@ elab (name := GameServer.Tactic.Branch) "Branch" t:tacticSeq : tactic => do
   -- Show an info whether the branch proofs all remaining goals.
   let gs ← Tactic.getUnsolvedGoals
   if gs.isEmpty then
-    logInfo "This branch finishes the proof."
+    trace[debug] "This branch finishes the proof."
   else
-    logInfo "This branch leaves open goals."
+    trace[debug] "This branch leaves open goals."
 
   let msgs ← Core.getMessageLog
   b.restore
@@ -525,7 +589,7 @@ elab (name := GameServer.Tactic.Hole) "Hole" t:tacticSeq : tactic => do
 
 /--
 Iterate recursively through the Syntax, replace `Hole` with `sorry` and remove all
-`Hint`/`Branch` occurences.
+`Hint`/`Branch` occurrences.
 -/
 def replaceHoles (tacs : Syntax) : Syntax :=
   match tacs with
@@ -539,7 +603,7 @@ where filterArgs (args : List Syntax) : List Syntax :=
     -- replace `Hole` with `sorry`.
     | Syntax.node info `GameServer.Tactic.Hole _ :: r =>
       Syntax.node info `Lean.Parser.Tactic.tacticSorry #[Syntax.atom info "sorry"] :: filterArgs r
-    -- delete all `Hint` and `Branch` occurences in the middle.
+    -- delete all `Hint` and `Branch` occurrences in the middle.
     | Syntax.node _ `GameServer.Tactic.Hint _ :: _ :: r
     | Syntax.node _ `GameServer.Tactic.Branch _ :: _ :: r =>
       filterArgs r
@@ -558,7 +622,7 @@ elab "Template" tacs:tacticSeq : tactic => do
   Tactic.evalTactic tacs
   let newTacs : TSyntax `Lean.Parser.Tactic.tacticSeq := ⟨replaceHoles tacs.raw⟩
   let template ← PrettyPrinter.ppCategory `Lean.Parser.Tactic.tacticSeq newTacs
-  logInfo s!"Template:\n{template}"
+  trace[debug] s!"Template:\n{template}"
   modifyLevel (←getCurLevelId) fun level => do
     return {level with template := s!"{template}"}
 
@@ -591,65 +655,6 @@ def GameLevel.setComputedInventory (level : GameLevel) :
 | .Definition, v => {level with definitions := {level.definitions with tiles := v}}
 | .Lemma, v =>      {level with lemmas      := {level.lemmas      with tiles := v}}
 
-/-- 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
-
-
 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
@@ -1048,7 +1053,6 @@ elab "MakeGame" : command => do
         modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
           return level.setComputedInventory inventoryType itemsArray
 
-
 /-! # Debugging tools -/
 
 -- /-- Print current game for debugging purposes. -/

server/GameServer/EnvExtensions.lean

@@ -67,7 +67,7 @@ structure InventoryTemplate where
   /-- Depends on the type:
   * Tactic: the tactic's name
   * Lemma: fully qualified lemma name
-  * Definition: no restrictions (preferrably the definions fully qualified name)
+  * Definition: no restrictions (preferably the definitions fully qualified name)
   -/
   name: Name
   /-- Only for Lemmas. To sort them into tabs -/
@@ -386,8 +386,13 @@ def modifyCurWorld (fn : World → m World) [MonadError m] : m Unit := do
     return {game with worlds := {game.worlds with nodes := game.worlds.nodes.insert world.name (← fn world) }}
 
 def addLevel (level : GameLevel) [MonadError m] : m Unit := do
-  modifyCurWorld fun world => do
-    return {world with levels := world.levels.insert level.index level}
+  let worldId ← getCurWorldId
+  match ← getLevel? ⟨← getCurGameId, worldId, level.index⟩ with
+  | some _existingLevel =>
+    throwError m!"Level {level.index} already exists for world {worldId}!"
+  | none =>
+    modifyCurWorld fun world => do
+      return {world with levels := world.levels.insert level.index level}
 
 def getCurLevel [MonadError m] : m GameLevel := do
   let some level := (← getCurWorld).levels.find? (← getCurLevelIdx)

server/GameServer/FileWorker.lean

@@ -57,6 +57,17 @@ open JsonRpc
 
 section Elab
 
+def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
+    Elab.Command.CommandElabM Unit := do
+  modify fun st => { st with
+      messages := st.messages.add {
+        fileName := inputCtx.fileName
+        severity := MessageSeverity.error
+        pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
+        data     := s
+      }
+    }
+
 -- TODO: use HashSet for allowed tactics?
 /-- Find all tactics in syntax object that are forbidden according to a
 set `allowed` of allowed tactics. -/
@@ -65,7 +76,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
     Elab.Command.CommandElabM Unit := do
   match stx with
   | .missing => return ()
-  | .node info kind args =>
+  | .node _info _kind args =>
     for arg in args do
       findForbiddenTactics inputCtx levelParams arg
   | .atom info val =>
@@ -89,13 +100,17 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
           | some _ => pure () -- tactic is in the inventory, allow it.
         else if tac.disabled then
           addWarningMessage info s!"The tactic '{val}' is disabled in this level!"
-  | .ident info rawVal val preresolved =>
+  | .ident info _rawVal val _preresolved =>
       let ns ←
         try resolveGlobalConst (mkIdent val)
         catch | _ => pure [] -- catch "unknown constant" error
       for n in ns do
         let some (.thmInfo ..) := (← getEnv).find? n
-          | return () -- not a theroem -> ignore
+          | return () -- not a theorem -> ignore
+        -- Forbid the theorem we are proving currently
+        if n = levelParams.statementName then
+          addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
+
         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!"
@@ -105,14 +120,19 @@ 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) :=
-  modify fun st => { st with
-    messages := st.messages.add {
-      fileName := inputCtx.fileName
-      severity := MessageSeverity.warning
-      pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
-      data     := s
+  let difficulty := levelParams.difficulty
+  if difficulty > 0 then
+    modify fun st => { st with
+      messages := st.messages.add {
+        fileName := inputCtx.fileName
+        severity := if difficulty > 1 then MessageSeverity.error else MessageSeverity.warning
+        pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
+        data     := s
+      }
     }
-  }
+  else pure ()
+-- where addErrorMessage (info : SourceInfo) (s : MessageData) :=
+--   pure ()
 
 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
@@ -170,8 +190,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           parseResultRef.set (tacticStx, cmdParserState)
 
           -- Check for forbidden tactics
-          if levelParams.checkEnabled then
-            findForbiddenTactics inputCtx levelParams 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 #[]
@@ -273,7 +292,7 @@ where
     -- TODO(MH): check for interrupt with increased precision
     cancelTk.check
     /- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
-      while prefering newer versions over old ones. The former is necessary because we do
+      while preferring newer versions over old ones. The former is necessary because we do
       not explicitly clear older diagnostics, while the latter is necessary because we do
       not guarantee that diagnostics are emitted in order. Specifically, it may happen that
       we interrupted this elaboration task right at this point and a newer elaboration task
@@ -281,7 +300,7 @@ where
       the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
       because we cannot guarantee that no further diagnostics are emitted after clearing
       them. -/
-    -- NOTE(WN): this is *not* redundent even if there are no new diagnostics in this snapshot
+    -- NOTE(WN): this is *not* redundant even if there are no new diagnostics in this snapshot
     -- because empty diagnostics clear existing error/information squiggles. Therefore we always
     -- want to publish in case there was previously a message at this position.
     publishDiagnostics m snap.diagnostics.toArray ctx.hOut
@@ -393,7 +412,7 @@ section Initialization
     -- Set the search path
     Lean.searchPathRef.set paths
 
-    let env ← importModules [{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
+    let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
     -- return (env, paths)
 
     -- use empty header
@@ -533,7 +552,7 @@ section MainLoop
 
       set {s with levelParams := {s.levelParams with
         inventory := p.inventory,
-        checkEnabled := p.checkEnabled}}
+        difficulty := p.difficulty}}
       mainLoop
     | Message.notification method (some params) =>
       handleNotification method (toJson params)

server/GameServer/Game.lean

@@ -7,7 +7,7 @@ structure GameServerState :=
 (game : Name)
 (gameDir : String)
 (inventory : Array String)
-(checkEnabled : Bool)
+(difficulty : Nat)
 
 abbrev GameServerM := StateT GameServerState Server.Watchdog.ServerM
 
@@ -50,6 +50,7 @@ structure LevelInfo where
   descrText : Option String := none
   descrFormat : String := ""
   lemmaTab : Option String
+  displayName : Option String
   statementName : Option String
   template : Option String
 deriving ToJson, FromJson
@@ -79,8 +80,15 @@ structure DidOpenLevelParams where
   lemmas : Array InventoryTile
   definitions : Array InventoryTile
   inventory : Array String
-  /-- if true the server gives warnings for used tactics/lemmas that are not unlocked. -/
-  checkEnabled : Bool
+  /--
+  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 LoadDocParams where
@@ -90,7 +98,7 @@ deriving ToJson, FromJson
 
 structure SetInventoryParams where
   inventory : Array String
-  checkEnabled : Bool
+  difficulty : Nat
 deriving ToJson, FromJson
 
 def handleDidOpenLevel (params : Json) : GameServerM Unit := do
@@ -117,7 +125,8 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
       lemmas := lvl.lemmas.tiles
       definitions := lvl.definitions.tiles
       inventory := s.inventory
-      checkEnabled := s.checkEnabled
+      difficulty := s.difficulty
+      statementName := lvl.statementName
       : DidOpenLevelParams
     }
   }
@@ -160,7 +169,8 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
               match lvl.lemmas.tiles.find? (·.new) with
               | some tile => tile.category
               | none => none
-            statementName := match lvl.statementName with
+            statementName := lvl.statementName.toString
+            displayName := match lvl.statementName with
               | .anonymous => none
               | name => match (inventoryExt.getState env).find?
                   (fun x => x.name == name && x.type == .Lemma) with
@@ -189,7 +199,6 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
     --   return true
     | Message.request id "loadDoc" params =>
       let p ← parseParams LoadDocParams (toJson params)
-      let s ← get
       let c ← read
       let some doc ← getInventoryItem? p.name p.type
         | do
@@ -205,7 +214,7 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
     | Message.notification "$/game/setInventory" params =>
       let p := (← parseParams SetInventoryParams (toJson params))
       let s ← get
-      set {s with inventory := p.inventory, checkEnabled := p.checkEnabled}
+      set {s with inventory := p.inventory, difficulty := p.difficulty}
       let st ← read
       let workers ← st.fileWorkersRef.get
       for (_, fw) in workers do

server/GameServer/Utils.lean

@@ -0,0 +1,50 @@
+import Lean
+
+open Lean Meta Elab Tactic Command
+
+syntax showOptArg := atomic(" (" (&"strict" <|> &"verbose") " := " withoutPosition(term) ")")
+
+/--
+Lists all available options that can be used with `set_option`.
+
+Use `set_option (verbose := true)` to display more than just the option names.
+The form `#show_option id` will show only options that begin with `id`.
+
+Copied from `#help option` from mathlib.
+-/
+elab "#show_option" verbose:(ppSpace showOptArg)? id:(ppSpace Parser.rawIdent)? : command => do
+  let id := id.map (·.raw.getId.toString false)
+  let mut decls : Lean.RBMap _ _ compare := {}
+  for (name, decl) in show Lean.RBMap .. from ← getOptionDecls do
+    let name := name.toString false
+    if let some id := id then
+      if !id.isPrefixOf name then
+        continue
+    decls := decls.insert name decl
+  let mut msg := Format.nil
+  let opts ← getOptions
+  if decls.isEmpty then
+    match id with
+    | some id => throwError "no options start with {id}"
+    | none => throwError "no options found (!)"
+  for (name, decl) in decls do
+    let mut msg1 := match decl.defValue with
+    | .ofString val => s!"String := {repr val}"
+    | .ofBool val => s!"Bool := {repr val}"
+    | .ofName val => s!"Name := {repr val}"
+    | .ofNat val => s!"Nat := {repr val}"
+    | .ofInt val => s!"Int := {repr val}"
+    | .ofSyntax val => s!"Syntax := {repr val}"
+    if let some val := opts.find name then
+      msg1 := s!"{msg1}  (currently: {val})"
+    msg := match verbose with
+    | some opt =>
+      match opt with
+      | `(showOptArg| (verbose := true)) =>
+        msg ++ .nest 2 (f!"option {name} : {msg1}" ++ .line ++ decl.descr) ++ .line ++ .line
+      | _ =>
+        msg ++ (f!"{name}" ++ .line )
+    | none =>
+      msg ++ (f!"{name}" ++ .line )
+
+  logInfo msg

server/GameServer/Watchdog.lean

@@ -91,7 +91,7 @@ def createEnv (gameDir : String) (module : String) : IO Environment := do
   -- Set the search path
   Lean.searchPathRef.set paths
 
-  let env ← importModules [{ module := `Init : Import }, { module := module : Import }] {} 0
+  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
@@ -114,7 +114,7 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
     game := gameName,
     gameDir := gameDir,
     inventory := #[]
-    checkEnabled := false
+    difficulty := 0
     }
   let initRequest ← i.readLspRequestAs "initialize" InitializeParams
   -- We misuse the `rootUri` field to the gameName

server/index.mjs

@@ -8,28 +8,21 @@ import * as jsonrpcserver from 'vscode-ws-jsonrpc/server';
 import os from 'os';
 import anonymize from 'ip-anonymize';
 // import { importTrigger, importStatus } from './import.mjs'
+// import fs from 'fs'
 
-/** Preloaded games. The keys refer to the docker tags of the virtual machines.
- * The number `queueLength` determines how many instances of the docker container
- * get started before any user shows up to have them up and running immediately.
- * The values `name`, `module`, and `dir` are just used for development where we
- * use a project directory instead of a docker container.
+/**
 */
 const games = {
     "g/hhu-adam/robo": {
-        // module: "Game",  // The lean module's name. Defaults to "Game"
-        // name: "Adam",    // For the `Game "Adam"` tag in the games. Defaults to "MyGame"
         dir: "Robo",
         queueLength: 5
     },
     "g/hhu-adam/nng4": {
-        // module: "Game",
-        // name: "NNG",
         dir: "NNG4",
         queueLength: 5
     },
-    "g/local/game": {
-        dir: "game",
+    "g/hhu-adam/nng4-old": {
+        dir: "NNG4-OLD",
         queueLength: 0
     }
 }
@@ -61,51 +54,66 @@ const isDevelopment = environment === 'development'
 /** We keep queues of started Lean Server processes to be ready when a user arrives */
 const queue = {}
 
-function startServerProcess(tag) {
-    if (! games[tag]?.dir) {
-        console.error(`Unknown game: ${tag}`)
-        return
-    }
+function tag(owner, repo) {
+  return `g/${owner.toLowerCase()}/${repo.toLowerCase()}`
+}
 
-    let serverProcess
-    if (isDevelopment) {
-        let args = ["--server", path.join("../../../../", games[tag].dir)]
-        if (games[tag].module) {
-            args.push(games[tag].module)
-            if (games[tag].name) { args.push(games[tag].name) }
-        }
-        serverProcess = cp.spawn("./gameserver", args,
-            { cwd: path.join(__dirname, "./build/bin/") })
-    } else {
-        serverProcess =  cp.spawn("./bubblewrap.sh",
-            [games[tag].dir],
-            { cwd: __dirname })
+function startServerProcess(owner, repo) {
+  let game_dir = (owner == 'local') ?
+    repo : games[tag(owner, repo)]?.dir
+
+  if (owner == 'local') {
+    if(!isDevelopment) {
+      console.error(`No local games in production mode.`)
+      return
     }
-    serverProcess.on('error', error =>
-        console.error(`Launching Lean Server failed: ${error}`)
-    );
-    if (serverProcess.stderr !== null) {
-        serverProcess.stderr.on('data', data =>
-            console.error(`Lean Server: ${data}`)
-        );
-    }
-    return serverProcess
+    // TODO: This test does not work
+    // if (!fs.existsSync(path.join("../", game_dir))) {
+    //   console.error(`Game folder does not exists: ${game_dir}`)
+    //   return
+    // }
+  }
+
+  if (!game_dir) {
+    console.error(`Unknown game: ${tag(owner, repo)}`)
+    return
+  }
+
+  let serverProcess
+  if (isDevelopment) {
+    let args = ["--server", path.join("../../../../", game_dir)]
+    serverProcess = cp.spawn("./gameserver", args,
+        { cwd: path.join(__dirname, "./build/bin/") })
+  } else {
+    serverProcess =  cp.spawn("./bubblewrap.sh",
+      [game_dir],
+      { cwd: __dirname })
+  }
+  serverProcess.on('error', error =>
+    console.error(`Launching Lean Server failed: ${error}`)
+  )
+  if (serverProcess.stderr !== null) {
+    serverProcess.stderr.on('data', data =>
+      console.error(`Lean Server: ${data}`)
+    )
+  }
+  return serverProcess
 }
 
 /** start Lean Server processes to refill the queue */
-function fillQueue(tag) {
-    while (queue[tag].length < games[tag].queueLength) {
-        const serverProcess = startServerProcess(tag)
-        queue[tag].push(serverProcess)
+function fillQueue(owner, repo) {
+    while (queue[tag(owner, repo)].length < games[tag(owner, repo)].queueLength) {
+      const serverProcess = startServerProcess(tag(owner, repo))
+      queue[tag(owner, repo)].push(serverProcess)
     }
 }
 
-if (!isDevelopment) { // Don't use queue in development
-    for (let tag in games) {
-        queue[tag] = []
-        fillQueue(tag)
-    }
-}
+// if (!isDevelopment) { // Don't use queue in development
+//   for (let tag in games) {
+//     queue[tag] = []
+//     fillQueue(tag)
+//   }
+// }
 
 const urlRegEx = /^\/websocket\/g\/([\w.-]+)\/([\w.-]+)$/
 
@@ -114,18 +122,19 @@ wss.addListener("connection", function(ws, req) {
     if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; }
     const owner = reRes[1]
     const repo = reRes[2]
-    const tag = `g/${owner.toLowerCase()}/${repo.toLowerCase()}`
+    // const tag = `g/${owner.toLowerCase()}/${repo.toLowerCase()}`
 
-    if (isDevelopment && process.env.DEV_CONTAINER) {
-        tag = `g/local/game`
-    }
+    // // TODO
+    // if (isDevelopment && process.env.DEV_CONTAINER) {
+    //     tag = `g/local/game`
+    // }
 
     let ps;
-    if (!queue[tag] || queue[tag].length == 0) {
-        ps = startServerProcess(tag)
+    if (!queue[tag(owner, repo)] || queue[tag(owner, repo)].length == 0) {
+        ps = startServerProcess(owner, repo)
     } else {
-        ps = queue[tag].shift() // Pick the first Lean process; it's likely to be ready immediately
-        fillQueue(tag)
+        ps = queue[tag(owner, repo)].shift() // Pick the first Lean process; it's likely to be ready immediately
+        fillQueue(owner, repo)
     }
 
     socketCounter += 1;

server/lake-manifest.json

@@ -1 +1,4 @@
-{"version": 5, "packagesDir": "lake-packages", "packages": []}
+{"version": 6,
+ "packagesDir": "lake-packages",
+ "packages": [],
+ "name": "GameServer"}

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4:v4.1.0

server/test/test_statement.lean

@@ -13,13 +13,16 @@ Level 1
 Statement foo.bar : 5 ≤ 7 := by
   simp
 
--- Shows warning on `foo.bar₂`:
+Game "Test"
+World "TestW"
+Level 2 -- should warn if set to `1`
 
+-- Shows warning on `foo.bar₂`:
 Statement foo.bar2 : 3 ≤ 7 := by
   simp
 
 
-NewLemma foo.baz
+NewLemma foo.bar
 DisabledTactic tauto