bump to v4.4.0-rc1

Mobile option (template)

client/src/app.tsx

@@ -9,16 +9,33 @@ import '@fontsource/roboto/700.css';
 import './css/reset.css';
 import './css/app.css';
 import { MobileContext } from './components/infoview/context';
-import { useWindowDimensions } from './window_width';
+import { useMobile } from './hooks';
+import { AUTO_SWITCH_THRESHOLD, getWindowDimensions} from './state/preferences';
 import { connection } from './connection';
 
 export const GameIdContext = React.createContext<string>(undefined);
 
 function App() {
+  const { mobile, setMobile, lockMobile, setLockMobile } = useMobile();
+
   const params = useParams()
   const gameId = "g/" + params.owner + "/" + params.repo
-  const {width, height} = useWindowDimensions()
-  const [mobile, setMobile] = React.useState(width < 800)
+
+  const automaticallyAdjustLayout = () => {
+    const {width} = getWindowDimensions()
+    setMobile(width < AUTO_SWITCH_THRESHOLD)
+  }
+
+  React.useEffect(()=>{
+    if (!lockMobile){
+      void automaticallyAdjustLayout()
+      window.addEventListener('resize', automaticallyAdjustLayout)
+
+      return () => {
+        window.removeEventListener('resize', automaticallyAdjustLayout)
+      }
+    }
+  }, [lockMobile])
 
   React.useEffect(() => {
     connection.startLeanClient(gameId);
@@ -27,7 +44,7 @@ function App() {
   return (
     <div className="app">
       <GameIdContext.Provider value={gameId}>
-        <MobileContext.Provider value={{mobile, setMobile}}>
+        <MobileContext.Provider value={{mobile, setMobile, lockMobile, setLockMobile}}>
           <Outlet />
         </MobileContext.Provider>
       </GameIdContext.Provider>

client/src/components/app_bar.tsx

@@ -5,7 +5,7 @@ import * as React from 'react'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
   faArrowRight, faArrowLeft, faXmark, faBars, faCode,
-  faCircleInfo, faTerminal } from '@fortawesome/free-solid-svg-icons'
+  faCircleInfo, faTerminal, faMobileScreenButton, faDesktop, faGear } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from "../app"
 import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context"
 import { GameInfo, useGetGameInfoQuery } from '../state/api'
@@ -150,22 +150,23 @@ function InventoryButton({pageNumber, setPageNumber}) {
 }
 
 /** the navigation bar on the welcome page */
-export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo} : {
+export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo, togglePreferencesPopup} : {
   pageNumber: number,
   setPageNumber: any,
   gameInfo: GameInfo,
   toggleImpressum: any,
   toggleEraseMenu: any,
   toggleUploadMenu: any,
-  toggleInfo: any
+  toggleInfo: any,
+  togglePreferencesPopup: () => void;
 }) {
   const gameId = React.useContext(GameIdContext)
   const gameProgress = useAppSelector(selectProgress(gameId))
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile, setMobile} = React.useContext(MobileContext)
   const [navOpen, setNavOpen] = React.useState(false)
 
   return <div className="app-bar">
-    <div>
+    <div className='app-bar-left'>
       <Button inverted="false" title="back to games selection" to="/">
         <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
       </Button>
@@ -194,6 +195,9 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres
       <Button title="Impressum, privacy policy" inverted="true" to="" onClick={() => {toggleImpressum(); setNavOpen(false)}}>
         <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Impressum
       </Button>
+      <Button title="Preferences" inverted="true" to="" onClick={() => {togglePreferencesPopup(); setNavOpen(false)}}>
+         <FontAwesomeIcon icon={faGear} />&nbsp;Preferences
+       </Button>
     </div>
   </div>
 }
@@ -237,7 +241,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=
       </> :
       <>
         {/* DESKTOP VERSION */}
-        <div>
+        <div className='app-bar-left'>
           <HomeButton isDropdown={false} />
           <span className="app-bar-title">{worldTitle && `World: ${worldTitle}`}</span>
         </div>

client/src/components/infoview/context.ts

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

client/src/components/infoview/main.tsx

@@ -493,18 +493,20 @@ export function TypewriterInterface({props}) {
                       <Markdown>{props.data?.introduction}</Markdown>
                     </div>
                   }
-                  {mobile && <>
+                  {mobile &&
                     <Hints key={`hints-${i}`}
                       hints={step.hints} showHidden={showHelp.has(i)} step={i}
                       selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
-                    {i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
-                      <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
-                        Show more help!
-                      </Button>
-                    }
-                  </>
                   }
                   <GoalsTabs proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/>
+
+                  {mobile && i == proof.length - 1 &&
+                    hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
+                    <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
+                      Show more help!
+                    </Button>
+                  }
+
                   {/* Show a message that there are no goals left */}
                   {!step.goals.length && (
                     <div className="message information">
@@ -521,7 +523,7 @@ export function TypewriterInterface({props}) {
               }
             })}
             {mobile && completed &&
-              <div className="button-row">
+              <div className="button-row mobile">
                 {props.level >= props.worldSize ?
                   <Button to={`/${gameId}`}>
                     <FontAwesomeIcon icon={faHome} />&nbsp;Leave World

client/src/components/inventory.tsx

@@ -2,7 +2,8 @@ import * as React from 'react';
 import { useState, useEffect } from 'react';
 import '../css/inventory.css'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faLock, faBan } from '@fortawesome/free-solid-svg-icons'
+import { faLock, faBan, faCheck } from '@fortawesome/free-solid-svg-icons'
+import { faClipboard } from '@fortawesome/free-regular-svg-icons'
 import { GameIdContext } from '../app';
 import Markdown from './markdown';
 import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api';
@@ -10,10 +11,12 @@ import { selectDifficulty, selectInventory } from '../state/progress';
 import { store } from '../state/store';
 import { useSelector } from 'react-redux';
 
-export function Inventory({levelInfo, openDoc, enableAll=false} :
+export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=false} :
   {
     levelInfo: LevelInfo|InventoryOverview,
     openDoc: (props: {name: string, type: string}) => void,
+    lemmaTab: any,
+    setLemmaTab: any,
     enableAll?: boolean,
   }) {
 
@@ -31,19 +34,20 @@ export function Inventory({levelInfo, openDoc, enableAll=false} :
       }
       <h2>Theorems</h2>
       {levelInfo?.lemmas &&
-        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} defaultTab={levelInfo?.lemmaTab} level={levelInfo} enableAll={enableAll}/>
+        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} level={levelInfo} enableAll={enableAll} tab={lemmaTab} setTab={setLemmaTab}/>
       }
     </div>
   )
 }
 
-function InventoryList({items, docType, openDoc, defaultTab=null, level=undefined, enableAll=false} :
+function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, level=undefined, enableAll=false} :
   {
     items: InventoryTile[],
     docType: string,
     openDoc(props: {name: string, type: string}): void,
-    defaultTab? : string,
-    level? : LevelInfo|InventoryOverview,
+    tab?: any,
+    setTab?: any,
+    level?: LevelInfo|InventoryOverview,
     enableAll?: boolean,
   }) {
   // TODO: `level` is only used in the `useEffect` below to check if a new level has
@@ -59,8 +63,6 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
   }
   const categories = Array.from(categorySet).sort()
 
-  const [tab, setTab] = useState(defaultTab)
-
   // Add inventory items from local store as unlocked.
   // Items are unlocked if they are in the local store, or if the server says they should be
   // given the dependency graph. (OR-connection) (TODO: maybe add different logic for different
@@ -68,13 +70,6 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
   let inv: string[] = selectInventory(gameId)(store.getState())
   let modifiedItems : InventoryTile[] = items.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile)
 
-  useEffect(() => {
-    // If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading.
-    // `defaultTab` is `null` or `undefined` otherwise, in which case we don't want to switch.
-    if (defaultTab) {
-      setTab(defaultTab)
-    }}, [level])
-
   return <>
     {categories.length > 1 &&
       <div className="tab-bar">
@@ -89,21 +84,26 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
           (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName)
         ).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => {
             return <InventoryItem key={`${item.category}-${item.name}`}
+              item={item}
               showDoc={() => {openDoc({name: item.name, type: docType})}}
               name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false}
-              disabled={item.disabled} newly={item.new} enableAll={enableAll}/>
+              disabled={item.disabled} newly={item.new} enableAll={enableAll} />
         })
       }
     </div>
     </>
 }
 
-function InventoryItem({name, displayName, locked, disabled, newly, showDoc, enableAll=false}) {
+function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, enableAll=false}) {
   const icon = locked ? <FontAwesomeIcon icon={faLock} /> :
-               disabled ? <FontAwesomeIcon icon={faBan} /> : ""
+               disabled ? <FontAwesomeIcon icon={faBan} /> : item.st
   const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : ""
+  // Note: This is somewhat a hack as the statement of lemmas comes currently in the form
+  // `Namespace.statement_name (x y : Nat) : some type`
   const title = locked ? "Not unlocked yet" :
-                disabled ? "Not available in this level" : ""
+                disabled ? "Not available in this level" : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
+
+  const [copied, setCopied] = useState(false)
 
   const handleClick = () => {
     if (enableAll || !locked) {
@@ -111,7 +111,21 @@ function InventoryItem({name, displayName, locked, disabled, newly, showDoc, ena
     }
   }
 
-  return <div className={`item ${className}${enableAll ? ' enabled' : ''}`} onClick={handleClick} title={title}>{icon} {displayName}</div>
+  const copyItemName = (ev) => {
+    navigator.clipboard.writeText(displayName)
+    setCopied(true)
+    setInterval(() => {
+      setCopied(false)
+    }, 3000);
+    ev.stopPropagation()
+  }
+
+return <div className={`item ${className}${enableAll ? ' enabled' : ''}`} onClick={handleClick} title={title}>
+    {icon} {displayName}
+    <div className="copy-button" onClick={copyItemName}>
+      {copied ? <FontAwesomeIcon icon={faCheck} /> : <FontAwesomeIcon icon={faClipboard} />}
+    </div>
+  </div>
 }
 
 export function Documentation({name, type, handleClose}) {
@@ -131,16 +145,25 @@ export function Documentation({name, type, handleClose}) {
 export function InventoryPanel({levelInfo, visible = true}) {
   const gameId = React.useContext(GameIdContext)
 
+  const [lemmaTab, setLemmaTab] = useState(levelInfo?.lemmaTab)
+
   // The inventory is overlayed by the doc entry of a clicked item
   const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
   // Set `inventoryDoc` to `null` to close the doc
   function closeInventoryDoc() {setInventoryDoc(null)}
 
+    useEffect(() => {
+    // If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading.
+    // `defaultTab` is `null` or `undefined` otherwise, in which case we don't want to switch.
+    if (levelInfo?.lemmaTab) {
+      setLemmaTab(levelInfo?.lemmaTab)
+    }}, [levelInfo])
+
   return <div className={`column inventory-panel ${visible ? '' : 'hidden'}`}>
     {inventoryDoc ?
       <Documentation name={inventoryDoc.name} type={inventoryDoc.type} handleClose={closeInventoryDoc}/>
       :
-      <Inventory levelInfo={levelInfo} openDoc={setInventoryDoc} enableAll={true}/>
+      <Inventory levelInfo={levelInfo} openDoc={setInventoryDoc} enableAll={true} lemmaTab={lemmaTab} setLemmaTab={setLemmaTab}/>
     }
   </div>
 }

client/src/components/level.tsx

@@ -441,6 +441,7 @@ function PlayableLevel({impressum, setImpressum}) {
 function IntroductionPanel({gameInfo}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId} = useContext(WorldLevelIdContext)
+  const {mobile} = React.useContext(MobileContext)
 
   let text: Array<string> = gameInfo.data?.worlds.nodes[worldId].introduction.split(/\n(\s*\n)+/)
 
@@ -451,7 +452,7 @@ function IntroductionPanel({gameInfo}) {
           hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
       ))}
     </div>
-    <div className="button-row">
+    <div className={`button-row${mobile ? ' mobile' : ''}`}>
       {gameInfo.data?.worldSize[worldId] == 0 ?
         <Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
         <Button to={`/${gameId}/world/${worldId}/level/1`}>

client/src/components/popup/preferences.tsx

@@ -0,0 +1,55 @@
+import * as React from 'react'
+import { Input, Typography } from '@mui/material'
+import Markdown from '../markdown'
+import Switch from '@mui/material/Switch';
+import FormControlLabel from '@mui/material/FormControlLabel';
+
+import { IMobileContext } from "../infoview/context"
+
+interface PreferencesPopupProps extends IMobileContext{
+    handleClose: () => void
+} 
+
+export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile, handleClose }: PreferencesPopupProps) {
+    return <div className="modal-wrapper">
+        <div className="modal-backdrop" onClick={handleClose} />
+        <div className="modal">
+            <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
+            <Typography variant="body1" component="div" className="settings">
+                <div className='preferences-category'>
+                    <div className='category-title'>
+                        <h3>Mobile layout</h3>
+                    </div>
+                    <div className='preferences-item'>
+                        <FormControlLabel
+                            control={
+                            <Switch
+                                checked={mobile}
+                                onChange={() => setMobile(!mobile)}
+                                name="checked"
+                                color="primary"
+                            />
+                            }
+                            label="Enable"
+                            labelPlacement="start"
+                        />
+                    </div>
+                    <div className='preferences-item'>
+                        <FormControlLabel
+                            control={
+                            <Switch
+                                checked={!lockMobile}
+                                onChange={() => setLockMobile(!lockMobile)}
+                                name="checked"
+                                color="primary"
+                            />
+                            }
+                            label="Auto"
+                            labelPlacement="start"
+                        />
+                    </div>
+                </div>
+            </Typography>
+        </div>
+    </div>
+}

client/src/components/welcome.tsx

@@ -17,6 +17,7 @@ import { InfoPopup } from './popup/game_info'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
 import { RulesHelpPopup } from './popup/rules_help'
 import { UploadPopup } from './popup/upload'
+import { PreferencesPopup} from "./popup/preferences"
 import { WorldTreePanel } from './world_tree'
 
 import '../css/welcome.css'
@@ -63,7 +64,7 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string,
 /** main page of the game showing among others the tree of worlds/levels */
 function Welcome() {
   const gameId = React.useContext(GameIdContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile, setMobile, lockMobile, setLockMobile} = React.useContext(MobileContext)
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
@@ -77,15 +78,20 @@ function Welcome() {
   const [info, setInfo] = React.useState(false)
   const [rulesHelp, setRulesHelp] = React.useState(false)
   const [uploadMenu, setUploadMenu] = React.useState(false)
+  const [preferencesPopup, setPreferencesPopup] = React.useState(false)
+
   function closeEraseMenu()   {setEraseMenu(false)}
   function closeImpressum()   {setImpressum(false)}
   function closeInfo()        {setInfo(false)}
   function closeRulesHelp()   {setRulesHelp(false)}
   function closeUploadMenu()  {setUploadMenu(false)}
+  function closePreferencesPopup() {setPreferencesPopup(false)}
   function toggleEraseMenu()  {setEraseMenu(!eraseMenu)}
   function toggleImpressum()  {setImpressum(!impressum)}
   function toggleInfo()       {setInfo(!info)}
   function toggleUploadMenu() {setUploadMenu(!uploadMenu)}
+  function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)}
+
 
   // set the window title
   useEffect(() => {
@@ -101,7 +107,7 @@ function Welcome() {
   : <>
     <WelcomeAppBar pageNumber={pageNumber} setPageNumber={setPageNumber} gameInfo={gameInfo.data} toggleImpressum={toggleImpressum}
       toggleEraseMenu={toggleEraseMenu} toggleUploadMenu={toggleUploadMenu}
-      toggleInfo={toggleInfo} />
+      toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
     <div className="app-content">
       { mobile ?
           <div className="welcome mobile">
@@ -128,6 +134,7 @@ function Welcome() {
     {eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
     {uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
     {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
+    {preferencesPopup ? <PreferencesPopup mobile={mobile} setMobile={setMobile} lockMobile={lockMobile} setLockMobile={setLockMobile} handleClose={closePreferencesPopup}/> : null}
   </>
 }
 

client/src/components/world_tree.tsx

@@ -11,7 +11,7 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
-import { useAppDispatch } from '../hooks'
+import { useAppDispatch, useMobile } from '../hooks'
 import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
 import { store } from '../state/store'
 
@@ -197,13 +197,15 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
   const gameId = React.useContext(GameIdContext)
   const difficulty = useSelector(selectDifficulty(gameId))
   const dispatch = useAppDispatch()
+  const { mobile } = useMobile()
+
 
   function label(x : number) {
     return x == 0 ? 'none' : x == 1 ? 'relaxed' : 'regular'
   }
 
 
-  return <nav className="world-selection-menu">
+  return <nav className={`world-selection-menu${mobile ? '' : ' desktop'}`}>
     <div className="slider-wrap">
       <span className="difficulty-label">Rules
         <FontAwesomeIcon icon={rulesHelp ? faXmark : faCircleQuestion} className='helpButton' onClick={() => (setRulesHelp(!rulesHelp))}/>
@@ -213,7 +215,7 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
         title="Game Rules"
         min={0} max={2}
         aria-label="Game Rules"
-        defaultValue={difficulty}
+        value={difficulty}
         marks={[
           {value: 0, label: label(0)},
           {value: 1, label: label(1)},

client/src/css/app.css

@@ -105,11 +105,18 @@ em {
   position: relative;
   flex-direction: row;
   justify-content: space-between;
+  align-items: center;
   padding: 1.1em;
   filter: drop-shadow(0 0 5px rgba(0,0,0,0.5));
   z-index: 2;
 }
 
+.app-bar > .app-bar-left{
+  display: flex;
+  align-items: center;
+  gap: .5em;
+}
+
 .app-bar-title, .app-bar-subtitle {
   color: white;
   font-weight: 500;

client/src/css/inventory.css

@@ -26,7 +26,11 @@
 .inventory .item {
   background: #fff;
   border: solid 1px #777;
-  padding: .1em .5em;
+  padding-left: .5rem;
+  padding-right: 1.0rem;
+  padding-top: .1rem;
+  padding-bottom: .1rem;
+  position: relative;
 }
 
 .inventory .item.locked {
@@ -72,3 +76,21 @@
   color: black;
   border-bottom: 0.3em solid #999;
 }
+
+
+.inventory .item .copy-button {
+	min-width: 3px;
+	min-height: 3px;
+	display: inline-block;
+	color: #ccc;
+	font-size: 0.6em;
+	padding-right: .2rem;
+	vertical-align: top;
+	position: absolute;
+	top: 0;
+	right: 0;
+	height: 100%;
+	width: 1rem;
+	align-items: end;
+	text-align: end;
+}

client/src/css/level.css

@@ -232,6 +232,20 @@ td code  {
   height: 100%;
 } */
 
+.button-row.mobile {
+  margin: .5rem;
+  padding-top: .2rem;
+}
+
+.button-row.mobile .btn {
+  padding: .5em;
+  border-radius: .2em;
+  width: 100%;
+  margin: 0;
+  text-align: center;
+}
+
+
 .typewriter-interface {
   display: flex;
   flex-flow: column;
@@ -317,11 +331,6 @@ td code  {
   margin-right: 0;
 }
 
-#home-btn {
-  margin-right: .5em;
-  margin-left: 0;
-}
-
 .menu.dropdown .svg-inline--fa {
   width: 1.8rem;
 }

client/src/css/world_tree.css

@@ -49,7 +49,6 @@ svg .disabled {
 }
 
 .world-selection-menu {
-  position: absolute;
   right: 1em;
   top: 1em;
   /* margin: 1em; */
@@ -60,6 +59,10 @@ svg .disabled {
   filter: drop-shadow(4px 4px 5px rgba(0,0,0,0.5));
 }
 
+.world-selection-menu.desktop {
+  position: absolute;
+}
+
 .world-selection-menu .btn, .welcome .btn {
   min-width: 5em;
   text-align: center;

client/src/hooks.ts

@@ -1,6 +1,30 @@
 import { TypedUseSelectorHook, useDispatch, useSelector } from 'react-redux'
 import type { RootState, AppDispatch } from './state/store'
 
+import { setMobile as setMobileState, setLockMobile as setLockMobileState} from "./state/preferences"
+
 // Use throughout your app instead of plain `useDispatch` and `useSelector`
 export const useAppDispatch: () => AppDispatch = useDispatch
 export const useAppSelector: TypedUseSelectorHook<RootState> = useSelector
+
+export const useMobile = () => {
+  const dispatch = useAppDispatch();
+
+  const mobile = useAppSelector((state) => state.preferences.mobile);
+  const lockMobile = useAppSelector((state) => state.preferences.lockMobile);
+
+  const setMobile = (val: boolean) => {
+    dispatch(setMobileState(val));
+  };
+
+  const setLockMobile = (val: boolean) => {
+    dispatch(setLockMobileState(val));
+  };
+
+  return {
+    mobile,
+    setMobile,
+    lockMobile,
+    setLockMobile,
+  };
+};

client/src/state/api.ts

@@ -35,6 +35,7 @@ export interface InventoryTile {
   locked: boolean,
   new: boolean,
   hidden: boolean
+  altTitle: string,
 }
 
 export interface LevelInfo {

client/src/state/local_storage.ts

@@ -36,3 +36,24 @@ export async function saveState(state: any) {
     // Ignore
   }
 }
+
+const PREFERENCES_KEY = "preferences"
+
+/** Load from browser storage */
+export function loadPreferences() {
+  try {
+    const serializedState = localStorage.getItem(PREFERENCES_KEY);
+    return JSON.parse(serializedState)
+  } catch (e) {
+    return undefined;
+  }
+}
+
+export function savePreferences(state: any) {
+  try {
+    const serializedState = JSON.stringify(state)
+    localStorage.setItem(PREFERENCES_KEY, serializedState);
+  } catch (e) {
+    // Ignore
+  }
+}

client/src/state/preferences.ts

@@ -0,0 +1,37 @@
+import { createSlice } from "@reduxjs/toolkit";
+
+import { loadPreferences } from "./local_storage";
+
+interface PreferencesState {
+  mobile: boolean;
+  lockMobile: boolean;
+}
+
+export function getWindowDimensions() {
+  const {innerWidth: width, innerHeight: height } = window
+  return {width, height}
+}
+
+const { width } = getWindowDimensions()
+
+export const AUTO_SWITCH_THRESHOLD = 800
+
+const initialState: PreferencesState = loadPreferences() ?? {
+    mobile: width < AUTO_SWITCH_THRESHOLD,
+    lockMobile: false
+}
+
+export const preferencesSlice = createSlice({
+  name: "preferences",
+  initialState,
+  reducers: {
+    setMobile: (state, action) => {
+      state.mobile = action.payload;
+    },
+    setLockMobile: (state, action) => {
+      state.lockMobile = action.payload;
+    },
+  },
+});
+
+export const { setMobile, setLockMobile } = preferencesSlice.actions;

client/src/state/store.ts

@@ -7,13 +7,15 @@ import { debounce } from "debounce";
 import { connection } from '../connection'
 import { apiSlice } from './api'
 import { progressSlice } from './progress'
-import { saveState } from "./local_storage";
+import { preferencesSlice } from "./preferences"
+import { saveState, savePreferences } from "./local_storage";
 
 
 export const store = configureStore({
   reducer: {
     [apiSlice.reducerPath]: apiSlice.reducer,
     [progressSlice.name]: progressSlice.reducer,
+    [preferencesSlice.name]: preferencesSlice.reducer,
   },
   // Make connection available in thunks:
   middleware: getDefaultMiddleware =>
@@ -31,6 +33,7 @@ export const store = configureStore({
 store.subscribe(
   debounce(() => {
     saveState(store.getState()[progressSlice.name]);
+    savePreferences(store.getState()[preferencesSlice.name]);
   }, 800)
 );
 

client/src/window_width.tsx

@@ -1,21 +0,0 @@
-import {useState, useEffect} from 'react'
-
-function getWindowDimensions() {
-  const {innerWidth: width, innerHeight: height } = window
-  return {width, height}
-}
-
-export function useWindowDimensions() {
-  const [windowDimensions, setWindowDimensions] = useState(getWindowDimensions())
-
-  useEffect(() => {
-    function handleResize() {
-      setWindowDimensions(getWindowDimensions())
-    }
-    window.addEventListener('resize', handleResize)
-    return () => window.removeEventListener('resize', handleResize)
-
-  }, [])
-
-  return windowDimensions
-}

package-lock.json

@@ -13,6 +13,10 @@
         "@emotion/styled": "^11.10.5",
         "@fontsource/roboto": "^4.5.8",
         "@fontsource/roboto-mono": "^4.5.8",
+        "@fortawesome/fontawesome-svg-core": "^6.5.1",
+        "@fortawesome/free-regular-svg-icons": "^6.5.1",
+        "@fortawesome/free-solid-svg-icons": "^6.5.1",
+        "@fortawesome/react-fontawesome": "^0.2.0",
         "@leanprover/infoview": "^0.4.3",
         "@mui/icons-material": "^5.11.0",
         "@mui/material": "^5.11.1",
@@ -2221,231 +2225,6 @@
       "resolved": "https://registry.npmjs.org/@emotion/weak-memoize/-/weak-memoize-0.3.1.tgz",
       "integrity": "sha512-EsBwpc7hBUJWAsNPBmJy4hxWx12v6bshQsldrVmjxJoc3isbxhOrF2IcCpaXxfvq03NwkI7sbsOLXbYuqF/8Ww=="
     },
-    "node_modules/@esbuild/android-arm": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/android-arm/-/android-arm-0.18.20.tgz",
-      "integrity": "sha512-fyi7TDI/ijKKNZTUJAQqiG5T7YjJXgnzkURqmGj13C6dCqckZBLdl4h7bkhHt/t0WP+zO9/zwroDvANaOqO5Sw==",
-      "cpu": [
-        "arm"
-      ],
-      "optional": true,
-      "os": [
-        "android"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/android-arm64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/android-arm64/-/android-arm64-0.18.20.tgz",
-      "integrity": "sha512-Nz4rJcchGDtENV0eMKUNa6L12zz2zBDXuhj/Vjh18zGqB44Bi7MBMSXjgunJgjRhCmKOjnPuZp4Mb6OKqtMHLQ==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "android"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/android-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/android-x64/-/android-x64-0.18.20.tgz",
-      "integrity": "sha512-8GDdlePJA8D6zlZYJV/jnrRAi6rOiNaCC/JclcXpB+KIuvfBN4owLtgzY2bsxnx666XjJx2kDPUmnTtR8qKQUg==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "android"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/darwin-arm64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/darwin-arm64/-/darwin-arm64-0.18.20.tgz",
-      "integrity": "sha512-bxRHW5kHU38zS2lPTPOyuyTm+S+eobPUnTNkdJEfAddYgEcll4xkT8DB9d2008DtTbl7uJag2HuE5NZAZgnNEA==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "darwin"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/darwin-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/darwin-x64/-/darwin-x64-0.18.20.tgz",
-      "integrity": "sha512-pc5gxlMDxzm513qPGbCbDukOdsGtKhfxD1zJKXjCCcU7ju50O7MeAZ8c4krSJcOIJGFR+qx21yMMVYwiQvyTyQ==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "darwin"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/freebsd-arm64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/freebsd-arm64/-/freebsd-arm64-0.18.20.tgz",
-      "integrity": "sha512-yqDQHy4QHevpMAaxhhIwYPMv1NECwOvIpGCZkECn8w2WFHXjEwrBn3CeNIYsibZ/iZEUemj++M26W3cNR5h+Tw==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "freebsd"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/freebsd-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/freebsd-x64/-/freebsd-x64-0.18.20.tgz",
-      "integrity": "sha512-tgWRPPuQsd3RmBZwarGVHZQvtzfEBOreNuxEMKFcd5DaDn2PbBxfwLcj4+aenoh7ctXcbXmOQIn8HI6mCSw5MQ==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "freebsd"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-arm": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-arm/-/linux-arm-0.18.20.tgz",
-      "integrity": "sha512-/5bHkMWnq1EgKr1V+Ybz3s1hWXok7mDFUMQ4cG10AfW3wL02PSZi5kFpYKrptDsgb2WAJIvRcDm+qIvXf/apvg==",
-      "cpu": [
-        "arm"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-arm64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-arm64/-/linux-arm64-0.18.20.tgz",
-      "integrity": "sha512-2YbscF+UL7SQAVIpnWvYwM+3LskyDmPhe31pE7/aoTMFKKzIc9lLbyGUpmmb8a8AixOL61sQ/mFh3jEjHYFvdA==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-ia32": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-ia32/-/linux-ia32-0.18.20.tgz",
-      "integrity": "sha512-P4etWwq6IsReT0E1KHU40bOnzMHoH73aXp96Fs8TIT6z9Hu8G6+0SHSw9i2isWrD2nbx2qo5yUqACgdfVGx7TA==",
-      "cpu": [
-        "ia32"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-loong64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-loong64/-/linux-loong64-0.18.20.tgz",
-      "integrity": "sha512-nXW8nqBTrOpDLPgPY9uV+/1DjxoQ7DoB2N8eocyq8I9XuqJ7BiAMDMf9n1xZM9TgW0J8zrquIb/A7s3BJv7rjg==",
-      "cpu": [
-        "loong64"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-mips64el": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-mips64el/-/linux-mips64el-0.18.20.tgz",
-      "integrity": "sha512-d5NeaXZcHp8PzYy5VnXV3VSd2D328Zb+9dEq5HE6bw6+N86JVPExrA6O68OPwobntbNJ0pzCpUFZTo3w0GyetQ==",
-      "cpu": [
-        "mips64el"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-ppc64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-ppc64/-/linux-ppc64-0.18.20.tgz",
-      "integrity": "sha512-WHPyeScRNcmANnLQkq6AfyXRFr5D6N2sKgkFo2FqguP44Nw2eyDlbTdZwd9GYk98DZG9QItIiTlFLHJHjxP3FA==",
-      "cpu": [
-        "ppc64"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-riscv64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-riscv64/-/linux-riscv64-0.18.20.tgz",
-      "integrity": "sha512-WSxo6h5ecI5XH34KC7w5veNnKkju3zBRLEQNY7mv5mtBmrP/MjNBCAlsM2u5hDBlS3NGcTQpoBvRzqBcRtpq1A==",
-      "cpu": [
-        "riscv64"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/linux-s390x": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/linux-s390x/-/linux-s390x-0.18.20.tgz",
-      "integrity": "sha512-+8231GMs3mAEth6Ja1iK0a1sQ3ohfcpzpRLH8uuc5/KVDFneH6jtAJLFGafpzpMRO6DzJ6AvXKze9LfFMrIHVQ==",
-      "cpu": [
-        "s390x"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
     "node_modules/@esbuild/linux-x64": {
       "version": "0.18.20",
       "resolved": "https://registry.npmjs.org/@esbuild/linux-x64/-/linux-x64-0.18.20.tgz",
@@ -2461,96 +2240,6 @@
         "node": ">=12"
       }
     },
-    "node_modules/@esbuild/netbsd-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/netbsd-x64/-/netbsd-x64-0.18.20.tgz",
-      "integrity": "sha512-iO1c++VP6xUBUmltHZoMtCUdPlnPGdBom6IrO4gyKPFFVBKioIImVooR5I83nTew5UOYrk3gIJhbZh8X44y06A==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "netbsd"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/openbsd-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/openbsd-x64/-/openbsd-x64-0.18.20.tgz",
-      "integrity": "sha512-e5e4YSsuQfX4cxcygw/UCPIEP6wbIL+se3sxPdCiMbFLBWu0eiZOJ7WoD+ptCLrmjZBK1Wk7I6D/I3NglUGOxg==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "openbsd"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/sunos-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/sunos-x64/-/sunos-x64-0.18.20.tgz",
-      "integrity": "sha512-kDbFRFp0YpTQVVrqUd5FTYmWo45zGaXe0X8E1G/LKFC0v8x0vWrhOWSLITcCn63lmZIxfOMXtCfti/RxN/0wnQ==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "sunos"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/win32-arm64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/win32-arm64/-/win32-arm64-0.18.20.tgz",
-      "integrity": "sha512-ddYFR6ItYgoaq4v4JmQQaAI5s7npztfV4Ag6NrhiaW0RrnOXqBkgwZLofVTlq1daVTQNhtI5oieTvkRPfZrePg==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "win32"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/win32-ia32": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/win32-ia32/-/win32-ia32-0.18.20.tgz",
-      "integrity": "sha512-Wv7QBi3ID/rROT08SABTS7eV4hX26sVduqDOTe1MvGMjNd3EjOz4b7zeexIR62GTIEKrfJXKL9LFxTYgkyeu7g==",
-      "cpu": [
-        "ia32"
-      ],
-      "optional": true,
-      "os": [
-        "win32"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
-    "node_modules/@esbuild/win32-x64": {
-      "version": "0.18.20",
-      "resolved": "https://registry.npmjs.org/@esbuild/win32-x64/-/win32-x64-0.18.20.tgz",
-      "integrity": "sha512-kTdfRcSiDfQca/y9QIkng02avJ+NCaQvrMejlsB3RRv5sE9rRoeBPISaZpKxHELzRxZyLvNts1P27W3wV+8geQ==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "win32"
-      ],
-      "engines": {
-        "node": ">=12"
-      }
-    },
     "node_modules/@floating-ui/core": {
       "version": "1.5.0",
       "resolved": "https://registry.npmjs.org/@floating-ui/core/-/core-1.5.0.tgz",
@@ -2596,33 +2285,45 @@
       "integrity": "sha512-KrJdmkqz6DszT2wV/bbhXef4r0hV3B0vw2mAqei8A2kRnvq+gcJLmmIeQ94vu9VEXrUQzos5M9lH1TAAXpRphw=="
     },
     "node_modules/@fortawesome/fontawesome-common-types": {
-      "version": "6.4.2",
-      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.4.2.tgz",
-      "integrity": "sha512-1DgP7f+XQIJbLFCTX1V2QnxVmpLdKdzzo2k8EmvDOePfchaIGQ9eCHj2up3/jNEbZuBqel5OxiaOJf37TWauRA==",
+      "version": "6.5.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.5.1.tgz",
+      "integrity": "sha512-GkWzv+L6d2bI5f/Vk6ikJ9xtl7dfXtoRu3YGE6nq0p/FFqA1ebMOAWg3XgRyb0I6LYyYkiAo+3/KrwuBp8xG7A==",
       "hasInstallScript": true,
       "engines": {
         "node": ">=6"
       }
     },
     "node_modules/@fortawesome/fontawesome-svg-core": {
-      "version": "6.4.2",
-      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-svg-core/-/fontawesome-svg-core-6.4.2.tgz",
-      "integrity": "sha512-gjYDSKv3TrM2sLTOKBc5rH9ckje8Wrwgx1CxAPbN5N3Fm4prfi7NsJVWd1jklp7i5uSCVwhZS5qlhMXqLrpAIg==",
+      "version": "6.5.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-svg-core/-/fontawesome-svg-core-6.5.1.tgz",
+      "integrity": "sha512-MfRCYlQPXoLlpem+egxjfkEuP9UQswTrlCOsknus/NcMoblTH2g0jPrapbcIb04KGA7E2GZxbAccGZfWoYgsrQ==",
       "hasInstallScript": true,
       "dependencies": {
-        "@fortawesome/fontawesome-common-types": "6.4.2"
+        "@fortawesome/fontawesome-common-types": "6.5.1"
+      },
+      "engines": {
+        "node": ">=6"
+      }
+    },
+    "node_modules/@fortawesome/free-regular-svg-icons": {
+      "version": "6.5.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/free-regular-svg-icons/-/free-regular-svg-icons-6.5.1.tgz",
+      "integrity": "sha512-m6ShXn+wvqEU69wSP84coxLbNl7sGVZb+Ca+XZq6k30SzuP3X4TfPqtycgUh9ASwlNh5OfQCd8pDIWxl+O+LlQ==",
+      "hasInstallScript": true,
+      "dependencies": {
+        "@fortawesome/fontawesome-common-types": "6.5.1"
       },
       "engines": {
         "node": ">=6"
       }
     },
     "node_modules/@fortawesome/free-solid-svg-icons": {
-      "version": "6.4.2",
-      "resolved": "https://registry.npmjs.org/@fortawesome/free-solid-svg-icons/-/free-solid-svg-icons-6.4.2.tgz",
-      "integrity": "sha512-sYwXurXUEQS32fZz9hVCUUv/xu49PEJEyUOsA51l6PU/qVgfbTb2glsTEaJngVVT8VqBATRIdh7XVgV1JF1LkA==",
+      "version": "6.5.1",
+      "resolved": "https://registry.npmjs.org/@fortawesome/free-solid-svg-icons/-/free-solid-svg-icons-6.5.1.tgz",
+      "integrity": "sha512-S1PPfU3mIJa59biTtXJz1oI0+KAXW6bkAb31XKhxdxtuXDiUIFsih4JR1v5BbxY7hVHsD1RKq+jRkVRaf773NQ==",
       "hasInstallScript": true,
       "dependencies": {
-        "@fortawesome/fontawesome-common-types": "6.4.2"
+        "@fortawesome/fontawesome-common-types": "6.5.1"
       },
       "engines": {
         "node": ">=6"
@@ -5077,81 +4778,6 @@
         }
       }
     },
-    "node_modules/@swc/core-darwin-arm64": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-darwin-arm64/-/core-darwin-arm64-1.3.95.tgz",
-      "integrity": "sha512-VAuBAP3MNetO/yBIBzvorUXq7lUBwhfpJxYViSxyluMwtoQDhE/XWN598TWMwMl1ZuImb56d7eUsuFdjgY7pJw==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "darwin"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/@swc/core-darwin-x64": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-darwin-x64/-/core-darwin-x64-1.3.95.tgz",
-      "integrity": "sha512-20vF2rvUsN98zGLZc+dsEdHvLoCuiYq/1B+TDeE4oolgTFDmI1jKO+m44PzWjYtKGU9QR95sZ6r/uec0QC5O4Q==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "darwin"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/@swc/core-linux-arm-gnueabihf": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-linux-arm-gnueabihf/-/core-linux-arm-gnueabihf-1.3.95.tgz",
-      "integrity": "sha512-oEudEM8PST1MRNGs+zu0cx5i9uP8TsLE4/L9HHrS07Ck0RJ3DCj3O2fU832nmLe2QxnAGPwBpSO9FntLfOiWEQ==",
-      "cpu": [
-        "arm"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/@swc/core-linux-arm64-gnu": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-linux-arm64-gnu/-/core-linux-arm64-gnu-1.3.95.tgz",
-      "integrity": "sha512-pIhFI+cuC1aYg+0NAPxwT/VRb32f2ia8oGxUjQR6aJg65gLkUYQzdwuUmpMtFR2WVf7WVFYxUnjo4UyMuyh3ng==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/@swc/core-linux-arm64-musl": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-linux-arm64-musl/-/core-linux-arm64-musl-1.3.95.tgz",
-      "integrity": "sha512-ZpbTr+QZDT4OPJfjPAmScqdKKaT+wGurvMU5AhxLaf85DuL8HwUwwlL0n1oLieLc47DwIJEMuKQkYhXMqmJHlg==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "linux"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
     "node_modules/@swc/core-linux-x64-gnu": {
       "version": "1.3.95",
       "resolved": "https://registry.npmjs.org/@swc/core-linux-x64-gnu/-/core-linux-x64-gnu-1.3.95.tgz",
@@ -5182,51 +4808,6 @@
         "node": ">=10"
       }
     },
-    "node_modules/@swc/core-win32-arm64-msvc": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-win32-arm64-msvc/-/core-win32-arm64-msvc-1.3.95.tgz",
-      "integrity": "sha512-YaP4x/aZbUyNdqCBpC2zL8b8n58MEpOUpmOIZK6G1SxGi+2ENht7gs7+iXpWPc0sy7X3YPKmSWMAuui0h8lgAA==",
-      "cpu": [
-        "arm64"
-      ],
-      "optional": true,
-      "os": [
-        "win32"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/@swc/core-win32-ia32-msvc": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-win32-ia32-msvc/-/core-win32-ia32-msvc-1.3.95.tgz",
-      "integrity": "sha512-w0u3HI916zT4BC/57gOd+AwAEjXeUlQbGJ9H4p/gzs1zkSHtoDQghVUNy3n/ZKp9KFod/95cA8mbVF9t1+6epQ==",
-      "cpu": [
-        "ia32"
-      ],
-      "optional": true,
-      "os": [
-        "win32"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
-    "node_modules/@swc/core-win32-x64-msvc": {
-      "version": "1.3.95",
-      "resolved": "https://registry.npmjs.org/@swc/core-win32-x64-msvc/-/core-win32-x64-msvc-1.3.95.tgz",
-      "integrity": "sha512-5RGnMt0S6gg4Gc6QtPUJ3Qs9Un4sKqccEzgH/tj7V/DVTJwKdnBKxFZfgQ34OR2Zpz7zGOn889xwsFVXspVWNA==",
-      "cpu": [
-        "x64"
-      ],
-      "optional": true,
-      "os": [
-        "win32"
-      ],
-      "engines": {
-        "node": ">=10"
-      }
-    },
     "node_modules/@swc/counter": {
       "version": "0.1.2",
       "resolved": "https://registry.npmjs.org/@swc/counter/-/counter-0.1.2.tgz",
@@ -8535,19 +8116,6 @@
       "resolved": "https://registry.npmjs.org/fs.realpath/-/fs.realpath-1.0.0.tgz",
       "integrity": "sha512-OO0pH2lK6a0hZnAdau5ItzHPI6pUlvI7jMVnxUQRtw4owF2wk8lOSabtGDCTP4Ggrg2MbGnWO9X8K1t4+fGMDw=="
     },
-    "node_modules/fsevents": {
-      "version": "2.3.3",
-      "resolved": "https://registry.npmjs.org/fsevents/-/fsevents-2.3.3.tgz",
-      "integrity": "sha512-5xoDfX+fL7faATnagmWPpbFtwh/R77WmMMqqHGS65C3vvB0YHrgF+B1YmZ3441tMj5n63k0212XNoJwzlhffQw==",
-      "hasInstallScript": true,
-      "optional": true,
-      "os": [
-        "darwin"
-      ],
-      "engines": {
-        "node": "^8.16.0 || ^10.6.0 || >=11.0.0"
-      }
-    },
     "node_modules/function-bind": {
       "version": "1.1.1",
       "resolved": "https://registry.npmjs.org/function-bind/-/function-bind-1.1.1.tgz",

package.json

@@ -10,6 +10,10 @@
     "@emotion/styled": "^11.10.5",
     "@fontsource/roboto": "^4.5.8",
     "@fontsource/roboto-mono": "^4.5.8",
+    "@fortawesome/fontawesome-svg-core": "^6.5.1",
+    "@fortawesome/free-regular-svg-icons": "^6.5.1",
+    "@fortawesome/free-solid-svg-icons": "^6.5.1",
+    "@fortawesome/react-fontawesome": "^0.2.0",
     "@leanprover/infoview": "^0.4.3",
     "@mui/icons-material": "^5.11.0",
     "@mui/material": "^5.11.1",

relay/bubblewrap.sh

@@ -1,5 +1,6 @@
 #/bin/bash
 
+# Note: This fails if there is no default toolchain installed
 ELAN_HOME=$(lake env printenv ELAN_HOME)
 
 # $1 : the game directory

server/GameServer/Commands.lean

@@ -1,23 +1,12 @@
-import GameServer.EnvExtensions
+import GameServer.Helpers
+import GameServer.Inventory
+import GameServer.Options
+import GameServer.SaveData
 
 open Lean Meta Elab Command
 
 set_option autoImplicit false
 
-/-- Let `MakeGame` print the reasons why the worlds depend on each other. -/
-register_option lean4game.showDependencyReasons : Bool := {
-  defValue := false
-  descr := "show reasons for calculated world dependencies."
-}
-
-/-- Let `MakeGame` print the reasons why the worlds depend on each other.
-
-Note: currently unused in favour of setting `set_option trace.debug true`. -/
-register_option lean4game.verbose : Bool := {
-  defValue := false
-  descr := "display more info messages to help developing the game."
-}
-
 /-! # Game metadata -/
 
 /-- Switch to the specified `Game` (and create it if non-existent). Example: `Game "NNG"` -/
@@ -52,13 +41,15 @@ elab "Title" t:str : command => do
 
 /-- Define the introduction of the current game/world/level. -/
 elab "Introduction" t:str : command => do
+  let intro := t.getString
   match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with introduction := t.getString}
-  | .World => modifyCurWorld  fun world => pure {world with introduction := t.getString}
-  | .Game => modifyCurGame  fun game => pure {game with introduction := t.getString}
+  | .Level => modifyCurLevel fun level => pure {level with introduction := intro}
+  | .World => modifyCurWorld  fun world => pure {world with introduction := intro}
+  | .Game => modifyCurGame  fun game => pure {game with introduction := intro}
 
 /-- Define the info of the current game. Used for e.g. credits -/
 elab "Info" t:str : command => do
+  let info:= t.getString
   match ← getCurLayer with
   | .Level =>
     logError "Can't use `Info` in a level!"
@@ -66,7 +57,7 @@ elab "Info" t:str : command => do
   | .World =>
     logError "Can't use `Info` in a world"
     pure ()
-  | .Game => modifyCurGame  fun game => pure {game with info := t.getString}
+  | .Game => modifyCurGame  fun game => pure {game with info := info}
 
 /-- Provide the location of the image for the current game/world/level.
 Paths are relative to the lean project's root. -/
@@ -90,10 +81,11 @@ elab "Image" t:str : command => do
 /-- Define the conclusion of the current game or current level if some
 building a level. -/
 elab "Conclusion" t:str : command => do
+  let conclusion := t.getString
   match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with conclusion := t.getString}
-  | .World => modifyCurWorld  fun world => pure {world with conclusion := t.getString}
-  | .Game => modifyCurGame  fun game => pure {game with conclusion := t.getString}
+  | .Level => modifyCurLevel fun level => pure {level with conclusion := conclusion}
+  | .World => modifyCurWorld  fun world => pure {world with conclusion := conclusion}
+  | .Game => modifyCurGame  fun game => pure {game with conclusion := conclusion}
 
 /-- A list of games that should be played before this one. Example `Prerequisites "NNG" "STG"`. -/
 elab "Prerequisites" t:str* : command => do
@@ -102,13 +94,15 @@ elab "Prerequisites" t:str* : command => do
 
 /-- Short caption for the game (1 sentence) -/
 elab "CaptionShort" t:str : command => do
+  let caption := t.getString
   modifyCurGame fun game => pure {game with
-    tile := {game.tile with short := t.getString}}
+    tile := {game.tile with short := caption}}
 
 /-- More detailed description what the game is about (2-4 sentences). -/
 elab "CaptionLong" t:str : command => do
+  let caption := t.getString
   modifyCurGame fun game => pure {game with
-    tile := {game.tile with long := t.getString}}
+    tile := {game.tile with long := caption}}
 
 /-- A list of Languages the game is translated to. For example `Languages "German" "English"`.
 NOTE: For the time being, only a single language is supported.
@@ -130,119 +124,12 @@ elab "CoverImage" t:str : command => do
 
 /-! # Inventory
 
-The inventory contains docs for tactics, lemmas, and definitions. These are all locked
+The inventory contains docs for tactics, theorems, and definitions. These are all locked
 in the first level and get enabled during the game.
 -/
 
 /-! ## Doc entries -/
 
-/-- Copied from `Mathlib.Tactic.HelpCmd`.
-
-Gets the initial string token in a parser description. For example, for a declaration like
-`syntax "bla" "baz" term : tactic`, it returns `some "bla"`. Returns `none` for syntax declarations
-that don't start with a string constant. -/
-partial def getHeadTk (e : Expr) : Option String :=
-  match (Expr.withApp e λ e a => (e.constName?.getD Name.anonymous, a)) with
-  | (``ParserDescr.node, #[_, _, p]) => getHeadTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getHeadTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getHeadTk p
-  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getHeadTk p
-  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
-  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => some tk
-  | (``Parser.withAntiquot, #[_, p]) => getHeadTk p
-  | (``Parser.leadingNode, #[_, _, p]) => getHeadTk p
-  | (``HAndThen.hAndThen, #[_, _, _, _, p, _]) => getHeadTk p
-  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk
-  | (``Parser.symbol, #[.lit (.strVal tk)]) => some tk
-  | _ => none
-
-/-- Modified from `#help` in `Mathlib.Tactic.HelpCmd` -/
-def getTacticDocstring (env : Environment) (name: Name) : CommandElabM (Option String) := do
-  let name := name.toString (escape := false)
-  let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {}
-
-  let catName : Name := `tactic
-  let catStx : Ident := mkIdent catName -- TODO
-  let some cat := (Parser.parserExtension.getState env).categories.find? catName
-    | throwErrorAt catStx "{catStx} is not a syntax category"
-  liftTermElabM <| Term.addCategoryInfo catStx catName
-  for (k, _) in cat.kinds do
-    let mut used := false
-    if let some tk := do getHeadTk (← (← env.find? k).value?) then
-      let tk := tk.trim
-      if name ≠ tk then -- was `!name.isPrefixOf tk`
-        continue
-      used := true
-      decls := decls.insert tk ((decls.findD tk #[]).push k)
-  for (_name, ks) in decls do
-    for k in ks do
-      if let some doc ← findDocString? env k then
-        return doc
-
-  logWarning <| m!"Could not find a docstring for tactic {name}, consider adding one " ++
-    m!"using `TacticDoc {name} \"some doc\"`"
-  return none
-
-/-- Retrieve the docstring associated to an inventory item. For Tactics, this
-is not guaranteed to work. -/
-def getDocstring (env : Environment) (name : Name) (type : InventoryType) :
-    CommandElabM (Option String) :=
-  match type with
-  -- for tactics it's a lookup following mathlib's `#help`. not guaranteed to be the correct one.
-  | .Tactic => getTacticDocstring env name
-  | .Lemma => findDocString? env name
-  -- TODO: for definitions not implemented yet, does it work?
-  | .Definition => findDocString? env name
-
-/-- Checks if `inventoryTemplateExt` contains an entry with `(type, name)` and yields
-a warning otherwise. If `template` is provided, it will add such an entry instead of yielding a
-warning.
-
-`ref` is the syntax piece. If `name` is not provided, it will use `ident.getId`.
-I used this workaround, because I needed a new name (with correct namespace etc)
-to be used, and I don't know how to create a new ident with same position but different name.
--/
-def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.getId)
-    (template : Option String := none) : CommandElabM Unit := do
-  -- note: `name` is an `Ident` (instead of `Name`) for the log messages.
-  let env ← getEnv
-  let n := name
-  -- Find a key with matching `(type, name)`.
-  match (inventoryTemplateExt.getState env).findIdx?
-    (fun x => x.name == n && x.type == type) with
-  -- Nothing to do if the entry exists
-  | some _ => pure ()
-  | none =>
-    match template with
-    -- Warn about missing documentation
-    | none =>
-      let docstring ← match (← getDocstring env name type) with
-      | some ds =>
-        logInfoAt ref (m!"Missing {type} Documentation. Using existing docstring. " ++
-        m!"Add {name}\nAdd `{type}Doc {name}` somewhere above this statement.")
-        pure s!"*(lean docstring)*\\\n{ds}"
-      | none =>
-        logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++
-        m!"somewhere above this statement.")
-        pure "(missing)"
-
-      -- We just add a dummy entry
-      modifyEnv (inventoryTemplateExt.addEntry · {
-        type := type
-        name := name
-        category := if type == .Lemma then s!"{n.getPrefix}" else ""
-        content := docstring})
-    -- Add the default documentation
-    | some s =>
-      modifyEnv (inventoryTemplateExt.addEntry · {
-        type := type
-        name := name
-        category := if type == .Lemma then s!"{n.getPrefix}" else ""
-        content := s })
-      logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++
-        m!"docstring) instead. If you want to write a different description, add " ++
-        m!"`{type}Doc {name}` somewhere above this statement.")
-
 /-- Documentation entry of a tactic. Example:
 
 ```
@@ -252,37 +139,40 @@ TacticDoc rw "`rw` stands for rewrite, etc. "
 * The identifier is the tactics name. Some need to be escaped like `«have»`.
 * The description is a string supporting Markdown.
  -/
-elab "TacticDoc" name:ident content:str : command =>
+elab doc:docComment ? "TacticDoc" name:ident content:str ? : command => do
+  let doc ← parseDocCommentLegacy doc content
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Tactic
     name := name.getId
     displayName := name.getId.toString
-    content := content.getString })
+    content := doc })
 
-/-- Documentation entry of a lemma. Example:
+/-- Documentation entry of a theorem. Example:
 
 ```
-LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
+TheoremDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 ```
 
-* The first identifier is used in the commands `[New/Only/Disabled]Lemma`.
-  It is preferably the true name of the lemma. However, this is not required.
+* The first identifier is used in the commands `[New/Only/Disabled]Theorem`.
+  It is preferably the true name of the theorem. However, this is not required.
 * The string following `as` is the displayed name (in the Inventory).
-* The identifier after `in` is the category to group lemmas by (in the Inventory).
+* The identifier after `in` is the category to group theorems by (in the Inventory).
 * The description is a string supporting Markdown.
 
 Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
-The lemma/definition to have the same fully qualified name as in mathlib.
+The theorem/definition to have the same fully qualified name as in mathlib.
  -/
-elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
+elab doc:docComment ? "TheoremDoc" name:ident "as" displayName:str "in" category:str content:str ? :
+    command => do
+  let doc ← parseDocCommentLegacy doc content
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Lemma
     name := name.getId
     category := category.getString
     displayName := displayName.getString
-    content := content.getString })
+    content := doc })
 -- TODO: Catch the following behaviour.
--- 1. if `LemmaDoc` appears in the same file as `Statement`, it will silently use
+-- 1. if `TheoremDoc` appears in the same file as `Statement`, it will silently use
 -- it but display the info that it wasn't found in `Statement`
 -- 2. if it appears in a later file, however, it will silently not do anything and keep
 -- the first one.
@@ -300,37 +190,25 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur
 * The description is a string supporting Markdown.
 
 Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
-The lemma/definition to have the same fully qualified name as in mathlib.
+The theorem/definition to have the same fully qualified name as in mathlib.
  -/
-elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
+elab doc:docComment ? "DefinitionDoc" name:ident "as" displayName:str template:str ? : command => do
+  let doc ← parseDocCommentLegacy doc template
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Definition
     name := name.getId,
     displayName := displayName.getString,
-    content := template.getString })
+    content := doc })
 
 /-! ## Add inventory items -/
 
-def getStatement (name : Name) : CommandElabM MessageData := do
-  return ← addMessageContextPartial (.ofPPFormat { pp := fun
-    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
-    | none     => return "that's a bug." })
-
--- Note: We use `String` because we can't send `MessageData` as json, but
--- `MessageData` might be better for interactive highlighting.
-/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`.
-
-Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
-`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
-def getStatementString (name : Name) : CommandElabM String := do
-  try
-    return ← (← getStatement name).toString
-  catch
-  | _ => throwError m!"Could not find {name} in context."
-  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.
+def checkCommandNotDuplicated (items : Array Name) (cmd := "Command") : CommandElabM Unit := do
+  if ¬ items.isEmpty then
+    logWarning s!"You should only use one `{cmd}` per level, but it takes multiple arguments: `{cmd} obj₁ obj₂ obj₃`!"
 
 /-- Declare tactics that are introduced by this level. -/
 elab "NewTactic" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).tactics.new) "NewTactic"
   for name in ↑args do
     checkInventoryDoc .Tactic name -- TODO: Add (template := "[docstring]")
   modifyCurLevel fun level => pure {level with
@@ -338,14 +216,16 @@ elab "NewTactic" args:ident* : command => do
 
 /-- Declare tactics that are introduced by this level but do not show up in inventory. -/
 elab "NewHiddenTactic" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).tactics.hidden) "NewHiddenTactic"
   for name in ↑args do
     checkInventoryDoc .Tactic name (template := "")
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with new := level.tactics.new ++ args.map (·.getId),
                                    hidden := level.tactics.hidden ++ args.map (·.getId)}}
 
-/-- Declare lemmas that are introduced by this level. -/
-elab "NewLemma" args:ident* : command => do
+/-- Declare theorems that are introduced by this level. -/
+elab "NewTheorem" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.new) "NewTheorem"
   for name in ↑args do
     try let _decl ← getConstInfo name.getId catch
       | _ => logErrorAt name m!"unknown identifier '{name}'."
@@ -355,6 +235,7 @@ elab "NewLemma" args:ident* : command => do
 
 /-- Declare definitions that are introduced by this level. -/
 elab "NewDefinition" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).definitions.new) "NewDefinition"
   for name in ↑args do checkInventoryDoc .Definition name -- TODO: Add (template := "[mathlib]")
   modifyCurLevel fun level => pure {level with
     definitions := {level.definitions with new := args.map (·.getId)}}
@@ -362,31 +243,36 @@ elab "NewDefinition" args:ident* : command => do
 /-- Declare tactics that are temporarily disabled in this level.
 This is ignored if `OnlyTactic` is set. -/
 elab "DisabledTactic" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).tactics.disabled) "DisabledTactic"
   for name in ↑args do checkInventoryDoc .Tactic name
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with disabled := args.map (·.getId)}}
 
-/-- Declare lemmas that are temporarily disabled in this level.
-This is ignored if `OnlyLemma` is set. -/
-elab "DisabledLemma" args:ident* : command => do
+/-- Declare theorems that are temporarily disabled in this level.
+This is ignored if `OnlyTheorem` is set. -/
+elab "DisabledTheorem" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.disabled) "DisabledTheorem"
   for name in ↑args  do checkInventoryDoc .Lemma name
   modifyCurLevel fun level => pure {level with
     lemmas := {level.lemmas with disabled := args.map (·.getId)}}
 
 /-- Declare definitions that are temporarily disabled in this level -/
 elab "DisabledDefinition" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).definitions.disabled) "DisabledDefinition"
   for name in ↑args do checkInventoryDoc .Definition name
   modifyCurLevel fun level => pure {level with
     definitions := {level.definitions with disabled := args.map (·.getId)}}
 
 /-- Temporarily disable all tactics except the ones declared here -/
 elab "OnlyTactic" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).tactics.only) "OnlyTactic"
   for name in ↑args do checkInventoryDoc .Tactic name
   modifyCurLevel fun level => pure {level with
     tactics := {level.tactics with only := args.map (·.getId)}}
 
-/-- Temporarily disable all lemmas except the ones declared here -/
-elab "OnlyLemma" args:ident* : command => do
+/-- Temporarily disable all theorems except the ones declared here -/
+elab "OnlyTheorem" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.only) "OnlyTheorem"
   for name in ↑args do checkInventoryDoc .Lemma name
   modifyCurLevel fun level => pure {level with
     lemmas := {level.lemmas with only := args.map (·.getId)}}
@@ -394,65 +280,66 @@ elab "OnlyLemma" args:ident* : command => do
 /-- Temporarily disable all definitions except the ones declared here.
 This is ignored if `OnlyDefinition` is set. -/
 elab "OnlyDefinition" args:ident* : command => do
+  checkCommandNotDuplicated ((←getCurLevel).definitions.only) "OnlyDefinition"
   for name in ↑args do checkInventoryDoc .Definition name
   modifyCurLevel fun level => pure {level with
     definitions := {level.definitions with only := args.map (·.getId)}}
 
-/-- Define which tab of Lemmas is opened by default. Usage: `LemmaTab "Nat"`.
+/-- Define which tab of Lemmas is opened by default. Usage: `TheoremTab "Nat"`.
 If omitted, the current tab will remain open. -/
-elab "LemmaTab"  category:str : command =>
+elab "TheoremTab"  category:str : command =>
+  modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
+
+
+/-! DEPRECATED -/
+
+elab doc:docComment ? "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str ? :
+    command => do
+  logWarning "Deprecated. Has been renamed to `TheoremDoc`"
+  let doc ← parseDocCommentLegacy doc content
+  modifyEnv (inventoryTemplateExt.addEntry · {
+    type := .Lemma
+    name := name.getId
+    category := category.getString
+    displayName := displayName.getString
+    content := doc })
+
+elab "NewLemma" args:ident* : command => do
+  logWarning "Deprecated. Has been renamed to `NewTheorem`"
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.new) "NewLemma"
+  for name in ↑args do
+    try let _decl ← getConstInfo name.getId catch
+      | _ => logErrorAt name m!"unknown identifier '{name}'."
+    checkInventoryDoc .Lemma name -- TODO: Add (template := "[mathlib]")
+  modifyCurLevel fun level => pure {level with
+    lemmas := {level.lemmas with new := args.map (·.getId)}}
+
+elab "DisabledLemma" args:ident* : command => do
+  logWarning "Deprecated. Has been renamed to `DisabledTheorem`"
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.disabled) "DisabledLemma"
+  for name in ↑args  do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with
+    lemmas := {level.lemmas with disabled := args.map (·.getId)}}
+
+elab "OnlyLemma" args:ident* : command => do
+  logWarning "Deprecated. Has been renamed to `OnlyTheorem`"
+  checkCommandNotDuplicated ((←getCurLevel).lemmas.only) "OnlyLemma"
+  for name in ↑args do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with
+    lemmas := {level.lemmas with only := args.map (·.getId)}}
+
+elab "LemmaTab"  category:str : command => do
+  logWarning "Deprecated. Has been renamed to `TheoremTab`"
   modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
 
 /-! # Exercise Statement -/
 
-/-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
-syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
--- TODO
-
--- TODO: Reuse the following code for checking available tactics in user code:
-structure UsedInventory where
-(tactics : HashSet Name := {})
-(definitions : HashSet Name := {})
-(lemmas : HashSet Name := {})
-
-partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : CommandElabM UsedInventory := do
-  match stx with
-  | .missing => return acc
-  | .node _info kind args =>
-    if kind == `GameServer.Tactic.Hint || kind == `GameServer.Tactic.Branch then return acc
-    return ← args.foldlM (fun acc arg => collectUsedInventory arg acc) acc
-  | .atom _info val =>
-    -- ignore syntax elements that do not start with a letter
-    -- and ignore some standard keywords
-    let allowed := ["with", "fun", "at", "only", "by"]
-    if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
-      let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-      return {acc with tactics := acc.tactics.insert val}
-    else
-      return acc
-  | .ident _info _rawVal val _preresolved =>
-      let ns ←
-        try resolveGlobalConst (mkIdent val)
-        catch | _ => pure [] -- catch "unknown constant" error
-      return ← ns.foldlM (fun acc n => do
-        if let some (.thmInfo ..) := (← getEnv).find? n then
-          return {acc with lemmas := acc.lemmas.insertMany ns}
-        else
-          return {acc with definitions := acc.definitions.insertMany ns}
-      ) acc
-
--- #check expandOptDocComment?
-
 /-- Define the statement of the current level. -/
 elab doc:docComment ? attrs:Parser.Term.attributes ?
     "Statement" statementName:ident ? sig:declSig val:declVal : command => do
   let lvlIdx ← getCurLevelIdx
 
-  let docContent : Option String := match doc with
-  | none => none
-  | some s => match s.raw[1] with
-    | .atom _ val => val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩))
-    | _           => none --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}"
+  let docContent ← parseDocComment doc
 
   -- Save the messages before evaluation of the proof.
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
@@ -553,23 +440,6 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
 
 /-! # Hints -/
 
-syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
-
-/-- Remove any spaces at the beginning of a new line -/
-partial def removeIndentation (s : String) : String :=
-  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
-    let c := s.get i
-    let i := s.next i
-    if s.atEnd i then
-      acc.push c
-    else if removeSpaces && c == ' ' then
-      loop i acc (removeSpaces := true)
-    else if c == '\n' then
-      loop i (acc.push c) (removeSpaces := true)
-    else
-      loop i (acc.push c)
-  loop ⟨0⟩ ""
-
 /-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
 see hints. The tactic does not affect the goal state.
 -/
@@ -683,26 +553,6 @@ elab "Template" tacs:tacticSeq : tactic => do
     return {level with template := s!"{template}"}
 
 
-
-open IO.FS System FilePath in
-/-- Copies the folder `images/` to `.lake/gamedata/images/` -/
-def copyImages : IO Unit := do
-  let target : FilePath := ".lake" / "gamedata"
-  if ← FilePath.pathExists "images" then
-    for file in ← walkDir "images" do
-      let outFile := target.join file
-      -- create the directories
-      if ← file.isDir then
-        createDirAll outFile
-      else
-        if let some parent := outFile.parent then
-          createDirAll parent
-        -- copy file
-        let content ← readBinFile file
-        writeBinFile outFile content
-
-
-
 -- TODO: Notes for testing if a declaration has the simp attribute
 
 -- -- Test: From zulip
@@ -721,139 +571,6 @@ def copyImages : IO Unit := do
 
 /-! # Make Game -/
 
-#eval IO.FS.createDirAll ".lake/gamedata/"
-
--- TODO: register all of this as ToJson instance?
-def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do
-  let game ← getCurGame
-  let env ← getEnv
-  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
-
-  if ← path.isDir then
-    IO.FS.removeDirAll path
-  IO.FS.createDirAll path
-
-  -- copy the images folder
-  copyImages
-
-  for (worldId, world) in game.worlds.nodes.toArray do
-    for (levelId, level) in world.levels.toArray do
-      IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
-
-  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
-
-  for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
-    for name in allItemsByType.findD inventoryType {} do
-      let some item ← getInventoryItem? name inventoryType
-        | throwError "Expected item to exist: {name}"
-      IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
-
-  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
-    (allItemsByType.findD type {}).toArray.mapM (fun name => do
-      let some item ← getInventoryItem? name type
-        | throwError "Expected item to exist: {name}"
-      return item.toTile)
-  let inventory : InventoryOverview := {
-    lemmas := ← getTiles .Lemma
-    tactics := ← getTiles .Tactic
-    definitions := ← getTiles .Definition
-    lemmaTab := none
-  }
-  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))
-
-
-def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
-| .Tactic => level.tactics
-| .Definition => level.definitions
-| .Lemma => level.lemmas
-
-def GameLevel.setComputedInventory (level : GameLevel) :
-    InventoryType → Array InventoryTile → GameLevel
-| .Tactic, v =>     {level with tactics     := {level.tactics     with tiles := v}}
-| .Definition, v => {level with definitions := {level.definitions with tiles := v}}
-| .Lemma, v =>      {level with lemmas      := {level.lemmas      with tiles := v}}
-
-partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name))
-      (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) :
-    HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do
-  match (newArrows.find? id, decendants.find? id) with
-  | (some _, some _) => return (newArrows, decendants)
-  | _ =>
-    let mut newArr := newArrows
-    let mut desc := decendants
-    desc := desc.insert id {} -- mark as worked in case of loops
-    newArr := newArr.insert id {} -- mark as worked in case of loops
-    let children := arrows.findD id {}
-    let mut trimmedChildren := children
-    let mut theseDescs := children
-    for child in children do
-      (newArr, desc) := removeTransitiveAux child arrows newArr desc
-      let childDescs := desc.findD child {}
-      theseDescs := theseDescs.insertMany childDescs
-      for d in childDescs do
-        trimmedChildren := trimmedChildren.erase d
-    desc := desc.insert id theseDescs
-    newArr := newArr.insert id trimmedChildren
-    return (newArr, desc)
-
-def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do
-  let mut newArr := {}
-  let mut desc := {}
-  for id in arrows.toArray.map Prod.fst do
-    (newArr, desc) := removeTransitiveAux id arrows newArr desc
-    if (desc.findD id {}).contains id then
-      logError <| m!"Loop at {id}. " ++
-        m!"This should not happen and probably means that `findLoops` has a bug."
-      -- DEBUG:
-      -- for ⟨x, hx⟩ in desc.toList do
-      --   m := m ++ m!"{x}: {hx.toList}\n"
-      -- logError m
-
-  return newArr
-
-/-- The recursive part of `findLoops`. Finds loops that appear as successors of `node`.
-
-For performance reason it returns a HashSet of visited
-nodes as well. This is filled with all nodes ever looked at as they cannot be
-part of a loop anymore. -/
-partial def findLoopsAux (arrows : HashMap Name (HashSet Name)) (node : Name)
-    (path : Array Name := #[]) (visited : HashSet Name := {}) :
-    Array Name × HashSet Name := Id.run do
-  let mut visited := visited
-  match path.getIdx? node with
-  | some i =>
-    -- Found a loop: `node` is already the iᵗʰ element of the path
-    return (path.extract i path.size, visited.insert node)
-  | none =>
-    for successor in arrows.findD node {} do
-      -- If we already visited the successor, it cannot be part of a loop anymore
-      if visited.contains successor then
-        continue
-      -- Find any loop involving `successor`
-      let (loop, _) := findLoopsAux arrows successor (path.push node) visited
-      visited := visited.insert successor
-      -- No loop found in the dependants of `successor`
-      if loop.isEmpty then
-        continue
-      -- Found a loop, return it
-      return (loop, visited)
-  return (#[], visited.insert node)
-
-/-- Find a loop in the graph and return it. Returns `[]` if there are no loops. -/
-partial def findLoops (arrows : HashMap Name (HashSet Name)) : List Name := Id.run do
-  let mut visited : HashSet Name := {}
-  for node in arrows.toArray.map (·.1) do
-    -- Skip a node if it was already visited
-    if visited.contains node then
-      continue
-    -- `findLoopsAux` returns a loop or `[]` together with a set of nodes it visited on its
-    -- search starting from `node`
-    let (loop, moreVisited) := (findLoopsAux arrows node (visited := visited))
-    visited := moreVisited
-    if !loop.isEmpty then
-      return loop.toList
-  return []
-
 /-- The worlds of a game are joint by dependencies. These are
 automatically computed but can also be defined with the syntax
 `Dependency World₁ → World₂ → World₃`. -/
@@ -1120,6 +837,7 @@ elab "MakeGame" : command => do
               name := item
               displayName := data.displayName
               category := data.category
+              altTitle := data.statement
               hidden := hiddenItems.contains item })
 
 
@@ -1139,6 +857,7 @@ elab "MakeGame" : command => do
             displayName := data.displayName
             category := data.category
             locked := false
+            altTitle := data.statement
             hidden := hiddenItems.contains item }
       itemsInWorld := itemsInWorld.insert worldId items
 
@@ -1158,7 +877,8 @@ elab "MakeGame" : command => do
             displayName := data.displayName
             category := data.category
             locked := false
-            hidden := levelInfo.hidden.contains item }
+            altTitle := data.statement
+            hidden := hiddenItems.contains item }
 
         -- add the exercise statement from the previous level
         -- if it was named
@@ -1171,6 +891,7 @@ elab "MakeGame" : command => do
               name := name
               displayName := data.displayName
               category := data.category
+              altTitle := data.statement
               locked := false }
 
         -- add marks for `disabled` and `new` lemmas here, so that they only apply to
@@ -1190,18 +911,16 @@ elab "MakeGame" : command => do
           return level.setComputedInventory inventoryType itemsArray
     allItemsByType := allItemsByType.insert inventoryType allItems
 
-  saveGameData allItemsByType
+  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
+    (allItemsByType.findD type {}).toArray.mapM (fun name => do
+      let some item ← getInventoryItem? name type
+        | throwError "Expected item to exist: {name}"
+      return item.toTile)
+  let inventory : InventoryOverview := {
+    lemmas := (← getTiles .Lemma).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
+    tactics := (← getTiles .Tactic).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
+    definitions := (← getTiles .Definition).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
+    lemmaTab := none
+  }
 
-/-! # Debugging tools -/
-
--- /-- Print current game for debugging purposes. -/
--- elab "PrintCurGame" : command => do
---   logInfo (toJson (← getCurGame))
-
-/-- Print current level for debugging purposes. -/
-elab "PrintCurLevel" : command => do
-  logInfo (repr (← getCurLevel))
-
-/-- Print levels for debugging purposes. -/
-elab "PrintLevels" : command => do
-  logInfo $ repr $ (← getCurWorld).levels.toArray
+  saveGameData allItemsByType inventory

server/GameServer/EnvExtensions.lean

@@ -106,6 +106,8 @@ structure InventoryTile where
   new := false
   /-- hide the item in the inventory display -/
   hidden := false
+  /-- hover text -/
+  altTitle : String := default
 deriving ToJson, FromJson, Repr, Inhabited
 
 def InventoryItem.toTile (item : InventoryItem) : InventoryTile := {
@@ -148,6 +150,12 @@ structure InventoryOverview where
   lemmaTab : Option String
 deriving ToJson, FromJson
 
+-- TODO: Reuse the following code for checking available tactics in user code:
+structure UsedInventory where
+(tactics : HashSet Name := {})
+(definitions : HashSet Name := {})
+(lemmas : HashSet Name := {})
+
 /-! ## Environment extensions for game specification -/
 
 /-- Register a (non-persistent) environment extension to hold the current level -/

server/GameServer/FileWorker.lean

@@ -478,6 +478,8 @@ section Initialization
     return (ctx,
     { doc             := doc
       initHeaderStx   := headerStx
+      currHeaderStx      := headerStx
+      importCachingTask? := none
       pendingRequests := RBMap.empty
       rpcSessions     := RBMap.empty
     })

server/GameServer/Helpers.lean

@@ -0,0 +1,190 @@
+import Lean
+
+/-! This document contains various things which cluttered `Commands.lean`. -/
+
+open Lean Meta Elab Command
+
+syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
+
+/-! ## Doc Comment Parsing -/
+
+/-- Read a doc comment and get its content. Return `""` if no doc comment available. -/
+def parseDocComment! (doc: Option (TSyntax `Lean.Parser.Command.docComment)) :
+    CommandElabM String := do
+  match doc with
+  | none =>
+    logWarning "Add a text to this command with `/-- yada yada -/ MyCommand`!"
+    pure ""
+  | some s => match s.raw[1] with
+    | .atom _ val => pure <| val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩))
+    | _           => pure "" --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}"
+
+/-- Read a doc comment and get its content. Return `none` if no doc comment available. -/
+def parseDocComment (doc: Option (TSyntax `Lean.Parser.Command.docComment)) :
+    CommandElabM <| Option String := do
+  match doc with
+  | none => pure none
+  | some _ => parseDocComment! doc
+
+
+/-- TODO: This is only used to provide some backwards compatibility and you can
+replace `parseDocCommentLegacy` with `parseDocComment` in the future. -/
+def parseDocCommentLegacy (doc: Option (TSyntax `Lean.Parser.Command.docComment))
+    (t : Option (TSyntax `str)) : CommandElabM <| String := do
+  match doc with
+  | none =>
+    match t with
+    | none =>
+      pure <| ← parseDocComment! doc
+    | some t =>
+      logWarningAt t "You should use the new Syntax:
+
+      /-- yada yada -/
+      YourCommand
+
+      instead of
+
+      YourCommand \"yada yada\"
+      "
+      pure t.getString
+  | some _ =>
+    match t with
+      | none =>
+        pure <| ← parseDocComment! doc
+      | some t =>
+        logErrorAt t "You must not provide both, a docstring and a string following the command!
+        Only use
+
+        /-- yada yada -/
+        YourCommand
+
+        and remove the string following it!"
+        pure <| ← parseDocComment! doc
+
+/-! ## Statement string -/
+
+def getStatement (name : Name) : CommandElabM MessageData := do
+  return ← addMessageContextPartial (.ofPPFormat { pp := fun
+    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
+    | none     => return "that's a bug." })
+
+-- Note: We use `String` because we can't send `MessageData` as json, but
+-- `MessageData` might be better for interactive highlighting.
+/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`.
+
+Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
+`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
+def getStatementString (name : Name) : CommandElabM String := do
+  try
+    return ← (← getStatement name).toString
+  catch
+  | _ => throwError m!"Could not find {name} in context."
+  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.
+
+/-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
+syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
+-- TODO
+
+
+/-- Remove any spaces at the beginning of a new line -/
+partial def removeIndentation (s : String) : String :=
+  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
+    let c := s.get i
+    let i := s.next i
+    if s.atEnd i then
+      acc.push c
+    else if removeSpaces && c == ' ' then
+      loop i acc (removeSpaces := true)
+    else if c == '\n' then
+      loop i (acc.push c) (removeSpaces := true)
+    else
+      loop i (acc.push c)
+  loop ⟨0⟩ ""
+
+
+/-! ## Loops in Graph-like construct
+
+TODO: Why are we not using graphs here but our own construct `HashMap Name (HashSet Name)`?
+-/
+
+partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name))
+      (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) :
+    HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do
+  match (newArrows.find? id, decendants.find? id) with
+  | (some _, some _) => return (newArrows, decendants)
+  | _ =>
+    let mut newArr := newArrows
+    let mut desc := decendants
+    desc := desc.insert id {} -- mark as worked in case of loops
+    newArr := newArr.insert id {} -- mark as worked in case of loops
+    let children := arrows.findD id {}
+    let mut trimmedChildren := children
+    let mut theseDescs := children
+    for child in children do
+      (newArr, desc) := removeTransitiveAux child arrows newArr desc
+      let childDescs := desc.findD child {}
+      theseDescs := theseDescs.insertMany childDescs
+      for d in childDescs do
+        trimmedChildren := trimmedChildren.erase d
+    desc := desc.insert id theseDescs
+    newArr := newArr.insert id trimmedChildren
+    return (newArr, desc)
+
+
+def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do
+  let mut newArr := {}
+  let mut desc := {}
+  for id in arrows.toArray.map Prod.fst do
+    (newArr, desc) := removeTransitiveAux id arrows newArr desc
+    if (desc.findD id {}).contains id then
+      logError <| m!"Loop at {id}. " ++
+        m!"This should not happen and probably means that `findLoops` has a bug."
+      -- DEBUG:
+      -- for ⟨x, hx⟩ in desc.toList do
+      --   m := m ++ m!"{x}: {hx.toList}\n"
+      -- logError m
+
+  return newArr
+
+/-- The recursive part of `findLoops`. Finds loops that appear as successors of `node`.
+
+For performance reason it returns a HashSet of visited
+nodes as well. This is filled with all nodes ever looked at as they cannot be
+part of a loop anymore. -/
+partial def findLoopsAux (arrows : HashMap Name (HashSet Name)) (node : Name)
+    (path : Array Name := #[]) (visited : HashSet Name := {}) :
+    Array Name × HashSet Name := Id.run do
+  let mut visited := visited
+  match path.getIdx? node with
+  | some i =>
+    -- Found a loop: `node` is already the iᵗʰ element of the path
+    return (path.extract i path.size, visited.insert node)
+  | none =>
+    for successor in arrows.findD node {} do
+      -- If we already visited the successor, it cannot be part of a loop anymore
+      if visited.contains successor then
+        continue
+      -- Find any loop involving `successor`
+      let (loop, _) := findLoopsAux arrows successor (path.push node) visited
+      visited := visited.insert successor
+      -- No loop found in the dependants of `successor`
+      if loop.isEmpty then
+        continue
+      -- Found a loop, return it
+      return (loop, visited)
+  return (#[], visited.insert node)
+
+/-- Find a loop in the graph and return it. Returns `[]` if there are no loops. -/
+partial def findLoops (arrows : HashMap Name (HashSet Name)) : List Name := Id.run do
+  let mut visited : HashSet Name := {}
+  for node in arrows.toArray.map (·.1) do
+    -- Skip a node if it was already visited
+    if visited.contains node then
+      continue
+    -- `findLoopsAux` returns a loop or `[]` together with a set of nodes it visited on its
+    -- search starting from `node`
+    let (loop, moreVisited) := (findLoopsAux arrows node (visited := visited))
+    visited := moreVisited
+    if !loop.isEmpty then
+      return loop.toList
+  return []

server/GameServer/Inventory.lean

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

server/GameServer/Options.lean

@@ -0,0 +1,17 @@
+import Lean
+
+/-! This document contains custom options available in the game. -/
+
+/-- Let `MakeGame` print the reasons why the worlds depend on each other. -/
+register_option lean4game.showDependencyReasons : Bool := {
+  defValue := false
+  descr := "show reasons for calculated world dependencies."
+}
+
+/-- Let `MakeGame` print the reasons why the worlds depend on each other.
+
+Note: currently unused in favour of setting `set_option trace.debug true`. -/
+register_option lean4game.verbose : Bool := {
+  defValue := false
+  descr := "display more info messages to help developing the game."
+}

server/GameServer/RpcHandlers.lean

@@ -46,8 +46,8 @@ partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) :
   | .bvar i1, .bvar i2 => if i1 == i2 then bij else none
   | .fvar i1, .fvar i2 => bij.insert? i1 i2
   | .mvar _, .mvar _ => bij
-  | .sort u1, .sort u2 => bij -- TODO?
-  | .const n1 ls1, .const n2 ls2 =>
+  | .sort _u1, .sort _u2 => bij -- TODO?
+  | .const n1 _ls1, .const n2 _ls2 =>
     if n1 == n2 then bij else none -- && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2)
   | .app f1 a1, .app f2 a2 =>
     some bij

server/GameServer/SaveData.lean

@@ -0,0 +1,55 @@
+import GameServer.EnvExtensions
+
+open Lean Meta Elab Command
+
+
+/-! ## Copy images -/
+
+open IO.FS System FilePath in
+/-- Copies the folder `images/` to `.lake/gamedata/images/` -/
+def copyImages : IO Unit := do
+  let target : FilePath := ".lake" / "gamedata"
+  if ← FilePath.pathExists "images" then
+    for file in ← walkDir "images" do
+      let outFile := target.join file
+      -- create the directories
+      if ← file.isDir then
+        createDirAll outFile
+      else
+        if let some parent := outFile.parent then
+          createDirAll parent
+        -- copy file
+        let content ← readBinFile file
+        writeBinFile outFile content
+
+
+-- TODO: I'm not sure this should be happening here...
+#eval IO.FS.createDirAll ".lake/gamedata/"
+
+-- TODO: register all of this as ToJson instance?
+def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
+    (inventory : InventoryOverview): CommandElabM Unit := do
+  let game ← getCurGame
+  let env ← getEnv
+  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
+
+  if ← path.isDir then
+    IO.FS.removeDirAll path
+  IO.FS.createDirAll path
+
+  -- copy the images folder
+  copyImages
+
+  for (worldId, world) in game.worlds.nodes.toArray do
+    for (levelId, level) in world.levels.toArray do
+      IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
+
+  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
+
+  for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
+    for name in allItemsByType.findD inventoryType {} do
+      let some item ← getInventoryItem? name inventoryType
+        | throwError "Expected item to exist: {name}"
+      IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
+
+  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))

server/GameServer/Watchdog.lean

@@ -103,7 +103,7 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
   let gameName := if args.length < 4 then defaultGameName else args[3]!
   let workerPath := "./gameserver"
   -- TODO: Do the following commands slow us down?
-  let srcSearchPath ← initSrcSearchPath (← getBuildDir)
+  let srcSearchPath ← initSrcSearchPath
   let references ← IO.mkRef (← loadReferences)
   let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
   let i ← maybeTee "wdIn.txt" false i

server/lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
+   "rev": "ce2db21d86502e00c4761da5ade58a61612de656",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0",
+   "inputRev": "v4.4.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "GameServer",

server/lakefile.lean

@@ -12,7 +12,7 @@ lean_lib GameServer
 
 @[default_target]
 lean_exe gameserver {
-  root := `Main
+  root := `GameServer
   supportInterpreter := true
 }
 

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0
+leanprover/lean4:v4.4.0-rc1