Merge branch 'refactor'

client/src/components/app_bar.tsx

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

client/src/components/infoview/context.ts

@@ -65,13 +65,9 @@ export const ProofStateContext = React.createContext<{
 export const MobileContext = React.createContext<{
   mobile : boolean,
   setMobile: React.Dispatch<React.SetStateAction<Boolean>>,
-  pageNumber: number,
-  setPageNumber: React.Dispatch<React.SetStateAction<Number>>
 }>({
   mobile : false,
   setMobile: () => {},
-  pageNumber: 0,
-  setPageNumber: () => {}
 })
 
 export const WorldLevelIdContext = React.createContext<{
@@ -108,10 +104,14 @@ export const InputModeContext = React.createContext<{
   typewriterMode: boolean,
   setTypewriterMode: React.Dispatch<React.SetStateAction<boolean>>,
   typewriterInput: string,
-  setTypewriterInput: React.Dispatch<React.SetStateAction<string>>
+  setTypewriterInput: React.Dispatch<React.SetStateAction<string>>,
+  lockInputMode: boolean,
+  setLockInputMode: React.Dispatch<React.SetStateAction<boolean>>,
 }>({
   typewriterMode: true,
   setTypewriterMode: () => {},
   typewriterInput: "",
   setTypewriterInput: () => {},
+  lockInputMode: false,
+  setLockInputMode: () => {},
 });

client/src/components/infoview/infoview.css

@@ -1,201 +0,0 @@
-
-.message {
-  margin: 10px 0;
-  padding: 5px 10px;
-  border-radius: 3px 3px 3px 3px;
-}
-.message.information, .message.info {
-  /* color: #059; */
-  color: #000;
-  background-color: #DDF6FF;
-}
-.message.warning {
-  color: #9F6000;
-  background-color: #FEEFB3;
-}
-.message.error {
-  color: #D8000C;
-  background-color: #FFBABA;
-}
-
-.message.deleted-hint {
-  background-color: #eee;
-  color: #777;
-  box-shadow: .0em .0em .5em .2em #eee;
- }
-
-.hyp-group {
-  margin-bottom: 0.3em;
-}
-
-.hyp-group-title, .goal-title {
-  font-family: var(--ff-primary);
-  font-size: 1.2rem;
-}
-
-.goals-section-title {
-  font-size: 1.5rem;
-  font-weight: 500;
-}
-
-.level-completed {
-  font-size: 1.8rem;
-  font-weight: 500;
-}
-
-.typewriter {
-  background: var(--clr-primary);
-  padding: 0.5em;
-  font-family: var(--ff-primary);
-  border-radius: 0.2em;
-  /* margin: 0.2em 0 0; */
-}
-
-.typewriter.disabled{
-  background: #bbb;
-}
-
-.typewriter.disabled .btn-inverted,
-.typewriter.disabled .mtk1 {
-  color: #777;
-}
-
-.typewriter.disabled .typewriter-input-wrapper,
-.typewriter.disabled .monaco-editor,
-.typewriter.disabled .monaco-editor-background,
-.typewriter.disabled .btn-inverted {
-  background-color: #eee;
-}
-
-.typewriter form {
-  display: flex;
-}
-
-.typewriter button, .undo-button {
-  display: block;
-  white-space: nowrap;
-  flex: 0;
-}
-
-.typewriter .typewriter-input-wrapper{
-  min-width: 0;
-  flex: 1;
-  padding: 0.4em .6em 0;
-  font-size: 1rem;
-  background: white;
-  display: flex;
-  flex-direction: column;
-}
-
-.typewriter-interface .proof .MuiCircularProgress-root {
-  left: 50%;
-  position: relative;
-  margin-left: -20px;
-  margin-bottom: 0.6em;
-}
-
-.typewriter .typewriter-input {
-  flex: 1;
-}
-
-/* Turn off some monaco decorations: */
-.typewriter-input .monaco-editor .view-overlays .current-line {
-  border: 0;
-}
-.typewriter-input .monaco-editor .scroll-decoration {
-  box-shadow: none;
-}
-
-.other-goals .goals-section-title, .other-goals summary, .other-goals summary .font-code {
-  color: #5191d1;
-}
-
-.goals-section {
-  display: flex;
-  flex-direction: row;
-}
-
-.goals-section div {
-  flex-grow: 1;
-}
-
-#current-proof, #main-assumptions {
-  margin-right: 0.8em;
-}
-
-#current-proof, #other-goals {
-  margin-left: 0.8em;
-}
-
-.proof-display {
-  max-height: 6em;
-  overflow-y: auto;
-  overscroll-behavior-y: contain;
-  scroll-snap-type: y proximity;
-  color: #ccc;
-
-}
-
-.proof-display div:nth-last-child(4) {
-  color: #999;
-}
-
-.proof-display div:nth-last-child(3) {
-  color: #666;
-}
-
-.proof-display div:nth-last-child(2) {
-  color: #333;
-}
-
-.proof-display div:nth-last-child(1) {
-  color: #000;
-  scroll-snap-align: end;
-}
-
-.proof-display-wrapper {
-  background-color: #f0f0f0;
-  border-radius: 1em;
-  padding: 0.6em;
-}
-
-
-/* Push the goals to the bottom for now, until we insert the proof history above. */
-.typewriter-interface .content {
-  display: flex;
-  flex-direction: column;
-  scroll-behavior: smooth;
-}
-
-/* TODO this is in the wrong file */
-.chat {
-  scroll-behavior: smooth;
-}
-
-.typewriter-interface .content .tmp-pusher {
-  flex: 1;
-}
-
-.exercise .command {
-  background-color: #bbb;
-  padding: .5em;
-  border-radius: .2em;
-  /* TODO: It seems my browsers merge the margings of the proof steps,
-  so that it only shows once 0.5rem instead of twice. Thus have 1.5 here now.
-  */
-  margin-bottom: 1.5rem;
-  display: flex;
-  flex-direction: row;
-}
-
-.exercise .command-text {
-  flex: 1;
-  background-color: #fff;
-  font-family: "Droid Sans Mono", "monospace", monospace;
-  font-size: 14px;
-  padding: 0.4em .6em 0;
-}
-
-.undo-button {
-  color: #888;
-}

client/src/components/infoview/main.tsx

@@ -6,7 +6,7 @@ import type { DidCloseTextDocumentParams, DidChangeTextDocumentParams, Location,
 import 'tachyons/css/tachyons.css';
 import '@vscode/codicons/dist/codicon.css';
 import '../../../../node_modules/lean4-infoview/src/infoview/index.css';
-import './infoview.css'
+import '../../css/infoview.css'
 
 import { LeanFileProgressParams, LeanFileProgressProcessingInfo, defaultInfoviewConfig, EditorApi, InfoviewApi } from '@leanprover/infoview-api';
 import { useClientNotificationEffect, useServerNotificationEffect, useEventResult, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util';

client/src/components/inventory.css

@@ -1,74 +0,0 @@
-.inventory, .documentation {
-  padding: 0 1em 1em 1em;
-}
-
-.inventory h2, .documentation h2, .documentation h1 {
-  font-size: 1.5em;
-  margin-top: 1em;
-  margin-bottom: .2em;
-}
-
-.documentation h1 {
-  font-weight: 900;
-}
-
-.documentation.hidden {
-  display: none;
-  transition: display 2s;
-}
-
-.inventory-list {
-  display: flex;
-  gap: .5em;
-  flex-wrap : wrap;
-}
-
-.inventory .item {
-  background: #fff;
-  border: solid 1px #777;
-  padding: .1em .5em;
-}
-
-.inventory .item.locked {
-  border: solid 1px #ccc;
-  color: #ccc;
-}
-
-.inventory .item.disabled {
-  color: #d92c2c;
-}
-
-.inventory .item.new {
-  background-color: rgb(255, 242, 190);
-}
-
-.inventory .item:not(.locked), .inventory .item.enabled {
-  cursor: pointer;
-}
-
-.tab-bar {
-  border-bottom: 0.1em solid var(--clr-dark-gray);
-  margin-bottom: 0.5em;
-}
-
-.tab {
-  color: var(--clr-darker-gray);
-  line-height: inherit;
-  text-decoration: none;
-  padding: 0.2rem .6em;
-  font-size: 1rem;
-  margin: 0 .1em;
-  border: 0;
-  cursor: pointer;
-  display: inline-block;
-}
-
-.tab-bar.current .tab.active {
-  color: black;
-  border-bottom: 0.3em solid var(--clr-primary);
-}
-
-.tab.active {
-  color: black;
-  border-bottom: 0.3em solid #999;
-}

client/src/components/inventory.tsx

@@ -1,6 +1,6 @@
 import * as React from 'react';
 import { useState, useEffect } from 'react';
-import './inventory.css'
+import '../css/inventory.css'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faLock, faBan } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from '../app';

client/src/components/landing_page.css

@@ -1,223 +0,0 @@
-/* @font-face {
-  font-family: 'Roboto Slab';
-  src: url('data/font/RobotoSlab.woff2') format('woff2');
-  font-weight: normal;
-  font-style: normal;
-} */
-
-html {
-  font-size: 16px;
-}
-
-body {
-  font-family: system-ui, -apple-system, "Segoe UI", Roboto, "Helvetica Neue", Arial, "Noto Sans", "Liberation Sans", sans-serif, "Apple Color Emoji", "Segoe UI Emoji", "Segoe UI Symbol", "Noto Color Emoji";
-}
-
-a {
-  text-decoration: none;
-}
-
-@viewport {
-  width: device-width ;
-  zoom: 1.0 ;
-}
-
-.landing-page {
-  width: 100%;
-}
-
-.game-list {
-  display: grid;
-  grid-gap: 40px;
-  grid-template-columns: repeat(auto-fit, minmax(400px, 1fr));
-  padding-left: 20px;
-  padding-right: 20px;
-  padding-top: 60px;
-  padding-bottom: 80px;
-}
-
-
-@media screen and (max-width: 440px) {
-  .game-list {
-    grid-template-columns: 100%;
-
-  }
-}
-.game {
-  cursor: pointer;
-  border: 1px solid rgb(140, 140, 140);
-  border-radius: 20px;
-  box-shadow: 5px 5px 8px rgb(140, 140, 140);
-  max-width: 500px;
-  display: flex;
-  flex-direction: column;
-  justify-content: space-between;
-  justify-self: center;
-  font-size: 1rem;
-
-}
-
-.image {
-  width: 100%;
-  height: 200px;
-  object-fit: cover;
-}
-
-div.image {
-  background: rgb(29,0,36);
-  background: linear-gradient(137deg, rgba(97,9,121,1) 0%, rgba(0,212,255,1) 100%);
-}
-
-.game .wrapper > :not(.image), .game .info {
-  margin-left: 10px;
-  margin-right: 10px;
-}
-
-.short-description p, .info p {
-  margin-block-start: 0;
-  margin-block-end: 0;
-
-}
-
-.short-description {
-  padding-top: 5px;
-  padding-bottom: 5px;
-  height: 6.5rem;
-}
-.game-stats {
-  display: block;
-}
-
-.info {
-  margin-top: 5px;
-  margin-bottom: 15px;
-  /* width: calc(100% - 20px); */
-  border-collapse: collapse;
-}
-
-.info tr {
-  border-top: 1px solid rgb(200, 200, 200);
-  border-bottom: 1px solid rgb(200, 200, 200);
-}
-
-.info td {
-  padding-top: 5px;
-  padding-bottom: 5px;
-}
-
-.info td:nth-child(even) {
-  text-align: right;
-}
-
-.title {
-  font-size: 1.5rem;
-  font-weight: bold;
-  padding-top: 15px;
-  padding-bottom: 5px;
-}
-
-header {
-  background-repeat: none;
-  background-size: 100% 100%;
-  background-position: center;
-}
-
-#main-title {
-  padding: 20px;
-  align-items: center;
-  display: flex;
-  flex-direction: column;
-}
-
-#main-title h1 {
-  font-weight: bolder;
-  color: rgb(255, 255, 255);
-  font-size: calc(1.425rem + 2.1vw);
-  text-align: center;
-}
-
-#main-title p {
-  color: rgb(255, 255, 255);
-  font-weight: bold;
-  text-align: center;
-  max-width: 600px;
-  font-size: 1.25rem;
-}
-
-#main-title a {
-  color: rgb(255, 255, 255);
-  text-decoration: underline dotted;
-}
-
-#main-title a:hover {
-  color: rgb(218, 218, 218);
-}
-
-#main-title i {
-  font-style: italic;
-}
-
-header nav {
-  display: flex;
-  justify-content: flex-end;
-  padding: 8px;
-  background-color: rgba(0, 133, 162, .7);
-}
-
-footer {
-  background-color: rgba(0, 133, 162, 1);
-  /* display: flex;
-  flex-direction: row;
-  justify-content: flex-end; */
-  padding: 20px;
-}
-
-footer .link {
-  color: white;
-  cursor: pointer;
-  margin-left: 40px;
-  margin-right: 40px;
-}
-
-.github-link {
-  height: 24px; /* TODO: why do I need that? s*/
-}
-
-.landing-page > section {
-  padding-top: 40px;
-  padding-bottom: 40px;
-  padding-left: 40px;
-  padding-right: 40px;
-  font-size: 1.25rem;
-
-}
-
-.landing-page > section h2 {
-  font-size: calc(1.325rem + 0.9vw);
-  font-weight: bolder;
-}
-
-.landing-page > section:nth-of-type(odd) {
-  background-color: rgb(248, 249, 250)
-}
-
-.landing-page > section:nth-of-type(even) {
-  background-color: rgb(255, 255, 255)
-}
-
-@media screen and (min-width: 1300px) {
-  .landing-page > section .wrapper {
-    max-width: 1300px;
-    margin-left: calc(50% - 650px);
-    margin-right: calc(50% - 650px);
-  }
-}
-
-/* TODO: Adjust to 180px once there are more than two games */
-@media screen and (min-width: 1300px) {
-  .game-list {
-    max-width: 1300px;
-    margin-left: calc(50% - 650px);
-    margin-right: calc(50% - 650px);
-  }
-}

client/src/components/landing_page.tsx

@@ -6,7 +6,7 @@ import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
 
-import './landing_page.css'
+import '../css/landing_page.css'
 import coverRobo from '../assets/covers/formaloversum.png'
 import bgImage from '../assets/bg.jpg'
 

client/src/components/level.css

@@ -1,346 +0,0 @@
-.level-mobile {
-  height: 100%;
-  flex: 1;
-  min-height: 0;
-  /* display: flex; */
-}
-
-.hidden {
-  display: none;
-}
-
-.gutter {
-  background-color: #eee;
-
-  background-repeat: no-repeat;
-  background-position: 50%;
-}
-
-.gutter.gutter-vertical {
-  background-image: url('data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAB4AAAAFAQMAAABo7865AAAABlBMVEVHcEzMzMzyAv2sAAAAAXRSTlMAQObYZgAAABBJREFUeF5jOAMEEAIEEFwAn3kMwcB6I2AAAAAASUVORK5CYII=');
-}
-
-.gutter.gutter-horizontal {
-  background-image: url('data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAUAAAAeCAYAAADkftS9AAAAIklEQVQoU2M4c+bMfxAGAgYYmwGrIIiDjrELjpo5aiZeMwF+yNnOs5KSvgAAAABJRU5ErkJggg==');
-}
-
-.inventory-panel, .exercise-panel, .doc-panel, .introduction-panel {
-  height: 100%;
-  width: 100%;
-  overflow: auto;
-  position: relative;
-}
-
-.infoview {
-  padding-top: 1em;
-  padding-bottom: 0;
-}
-
-.infoview, .exercise-statement {
-  padding-left: .5em;
-  padding-right: .5em;
-}
-
-.exercise-statement {
-  padding-top: 1em;
-  padding-bottom: 1em;
-}
-
-.exercise-statement p {
-  margin: 0;
-}
-
-.exercise-statement .lean-code {
-  color: rgba(0, 32, 90, 0.87);
-  font-size: 12px; /* TODO: is the monaco font-size hardcoded? */
-}
-
-.conclusion {
-  padding: 1em;
-}
-
-.infoview {
-  padding-top: 0em;
-}
-
-.exercise {
-  flex: 1 1 auto;
-  display: flex;
-  flex-flow: column;
-}
-
-.codeview {
-  flex: 1 1 auto;
-  min-height: 192px;
-
-}
-
-.exercise h4 {
-  margin-top: 0;
-  margin-bottom: 0;
-}
-
-.input-mode-switch {
-  margin: 0;
-  display: flex;
-  flex-direction: row;
-  justify-content: flex-end;
-  gap: 1em;
-}
-
-.doc-panel {
-  background: #fafafa;
-}
-
-.doc-panel li {
-  border-bottom: 1px solid rgba(0, 0, 0, 0.12); /* This should be teh same colour as `divider` in Inventory.tsx */
-}
-
-.doc-panel li:first-of-type {
-  border-top: 1px solid rgb(0, 0, 0, 0.12); /* This should be teh same colour as `divider` in Inventory.tsx */
-}
-
-/* fix as Mui seems to set this to `nowrap`. */
-.MuiAccordionDetails-root {
-  white-space: normal;
-}
-
-/* TODO: Adjust Mathjax styling. 1em vertical is excessive. */
-mjx-container[jax="CHTML"][display="true"] {
-  margin: 0.2em 0 !important;
-}
-
-
-/* Styling tables for Markdown */
-.chat-panel table, .chat-panel th, .chat-panel td {
-  /* border: 1px solid rgb(0, 0, 0, 0.12); */
-  border-collapse: collapse;
-}
-
-.chat-panel th, .chat-panel td {
-  padding-left: .5em;
-  padding-right: .5em;
-}
-
-span.katex-display {
-  margin: 0;
-}
-
-p, table {
-  margin-block-start: 1em;
-  margin-block-end: 1em;
-  margin-inline-start: 0px;
-  margin-inline-end: 0px;
-}
-
-/* Prevent white spaces break inside a table. */
-td code  {
-  white-space:nowrap;
-}
-
-/* Styling in the editor while typing abbreviations such as "\alpha" */
-.abbreviation {
-  text-decoration: underline;
-}
-
-/* Styling in the left margin of the editor when processing */
-.processing {
-  background: linear-gradient(
-    to right,
-    rgba(255, 165, 0, 1) 0%,
-    rgba(255, 165, 0, 1) 30%,
-    transparent 30%,
-    transparent  100%
-  );
-}
-
-/* Styling in the left margin of the editor on error */
-.glyph-margin-error {
-  background: rgba(255, 0, 0, 1);
-}
-
-/***************************************/
-/* TODO: For development purposes only */
-/***************************************/
-/* .doc-panel {
-  border: 1px solid red;
-}
-
-.main-panel {
-  border: 1px solid rgb(41, 112, 0);
-}
-
-.info-panel {
-  border: 1px solid rgb(230, 122, 0);
-}
-
-.chat-panel {
-  border: 1px solid rgb(192, 18, 178);
-}
-
-.exercise {
-  border: 1px solid rgb(102, 243, 67);
-}
-
-.codeview {
-  border: 1px solid rgb(98, 148, 255);
-}
-
-.main-grid {
-  border: 1px solid rgb(255, 0, 0);
-  margin: 1px;
-} */
-
-.exercise {
-  height: 100%;
-}
-
-.chat {
-  flex: 1;
-  overflow-y: scroll;
-  margin-left: .5em;
-  margin-right: .5em;
-}
-
-.chat-panel {
-  padding-top: 0;
-  padding-bottom: 0;
-  overflow: hidden;
-  display: flex;
-  flex-direction: column;
-
-}
-
-.chat-panel .button-row {
-  /* width:100%; */
-  margin-left: .5em;
-  margin-right: .5em;
-  min-height: 2.5em;
-  border-top:  0.1em solid #aaa;
-}
-
-.chat-panel .btn {
-  margin-top: 1rem;
-  margin-bottom: 1rem;
-  margin-left: .5rem;
-  margin-right: .5rem;
-}
-
-/* .exercise-panel {
-  display: flex;
-  flex-flow: column;
-  height: 100%;
-} */
-
-.typewriter-interface {
-  display: flex;
-  flex-flow: column;
-  height: 100%;
-}
-
-.typewriter {
-  flex: 0 1 auto;
-}
-
-.typewriter-interface .content {
-  flex: 1 1 auto;
-  overflow-y: scroll;
-  padding: 0;
-}
-
-.exercise .step {
-  /* background-color: #e6f0f4; */
-  margin-top: .5rem;
-  margin-bottom: .5rem;
-  border-radius: 0.5rem;
-  padding: 0.5rem;
-  /* border: 3px dotted rgb(88, 131, 24); */
-}
-
-/* TODO: Is this still used anywhere? */
-.exercise .step .btn-help {
-  margin-top: 10px;
-}
-
-.chat .message {
-  margin-left: .5em;
-  margin-right: .5em;
-}
-
-.chat .recent {
-  box-shadow: .0em .0em .4em .1em #8cbbe9;
-}
-
-.exercise .step.selected .goal-tabs, .chat .selected {
-  /* border: 3px solid #5191d1; */
-  box-shadow: .0em .0em .4em .1em var(--clr-primary);
-}
-
-.introduction-panel {
-  max-width: 900px;
-  width: 80%;
-  margin-left: auto;
-  margin-right: auto;
-}
-
-.impressum {
-  background-color: #fff;
-  width: 100%;
-  height: 100%;
-  position: absolute;
-  top: 0;
-  z-index: 1;
-  padding: .5rem;
-}
-
-.menu.dropdown {
-  position: absolute;
-  display: flex;
-  flex-direction: column;
-  right: 0;
-  top: 100%;
-  background-color: #fff;
-  z-index: 1;
-  border-top: 1px solid rgba(0, 0, 0, 0.1);
-  border-bottom: 1px solid rgba(0, 0, 0, 0.1);
-  box-shadow: -.1rem .3rem .3rem 0 rgba(0, 0, 0, 0.1);
-}
-
-.menu.dropdown.hidden {
-  display: none;
-}
-
-#menu-btn {
-  padding: 0;
-  font-size: 1.3rem;
-  margin-left: .5em;
-  margin-right: 0;
-}
-
-#home-btn {
-  margin-right: .5em;
-  margin-left: 0;
-}
-
-.menu.dropdown .svg-inline--fa {
-  width: 1.8rem;
-}
-
-.tmp-pusher {
-  align-items: center;
-  display: flex;
-  justify-content: center;
-}
-
-.typewriter-interface .content, .world-image-container.empty {
-  background-color: #eee;
-}
-
-.typewriter-interface .proof {
-  background-color: #fff;
-}
-
-.toggle-width {
-  min-width: 40px;
-  text-align: center;
-}

client/src/components/level.tsx

@@ -4,7 +4,7 @@ import { useSelector, useStore } from 'react-redux'
 import Split from 'react-split'
 import { useParams } from 'react-router-dom'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faBars, faCode, faXmark, faHome, faCircleInfo, faArrowRight, faArrowLeft, faTerminal } from '@fortawesome/free-solid-svg-icons'
+import { faHome, faArrowRight } from '@fortawesome/free-solid-svg-icons'
 import { CircularProgress } from '@mui/material'
 import type { Location } from 'vscode-languageserver-protocol'
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
@@ -41,7 +41,7 @@ import '@fontsource/roboto/500.css'
 import '@fontsource/roboto/700.css'
 import 'lean4web/client/src/editor/infoview.css'
 import 'lean4web/client/src/editor/vscode.css'
-import './level.css'
+import '../css/level.css'
 import { LevelAppBar } from './app_bar'
 
 function Level() {
@@ -222,6 +222,8 @@ function PlayableLevel({impressum, setImpressum}) {
   // Only for mobile layout
   const [pageNumber, setPageNumber] = useState(0)
   const [typewriterMode, setTypewriterMode] = useState(true)
+  // set to true to prevent switching between typewriter and editor
+  const [lockInputMode, setLockInputMode] = useState(false)
   const [typewriterInput, setTypewriterInput] = useState("")
   const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
   const dispatch = useAppDispatch()
@@ -392,18 +394,16 @@ function PlayableLevel({impressum, setImpressum}) {
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
     <DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
       <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
-        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput}}>
+        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockInputMode, setLockInputMode}}>
           <ProofContext.Provider value={{proof, setProof}}>
             <EditorContext.Provider value={editorConnection}>
               <MonacoEditorContext.Provider value={editor}>
                 <LevelAppBar
+                  pageNumber={pageNumber} setPageNumber={setPageNumber}
                   isLoading={level.isLoading}
-                  lockEditorMode={level.data?.template !== null}
                   levelTitle={`${mobile ? '' : 'Level '}${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
                     (level?.data?.title && ` : ${level?.data?.title}`)}
-                  impressum={impressum}
-                    toggleImpressum={toggleImpressum}
-                  pageNumber={pageNumber} setPageNumber={setPageNumber} />
+                  toggleImpressum={toggleImpressum} />
                 {mobile?
                   // TODO: This is copied from the `Split` component below...
                   <>
@@ -471,7 +471,7 @@ function Introduction({impressum, setImpressum}) {
   }
 
   return <>
-    <LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Introduction" impressum={impressum} toggleImpressum={toggleImpressum}/>
+    <LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Introduction" toggleImpressum={toggleImpressum}/>
     {gameInfo.isLoading ?
       <div className="app-content loading"><CircularProgress /></div>
     : mobile ?

client/src/components/popup/erase.tsx

@@ -9,6 +9,15 @@ import { deleteProgress, selectProgress } from '../../state/progress'
 import { downloadFile } from '../world_tree'
 import { Button } from '../button'
 
+/** download the current progress (i.e. what's saved in the browser store) */
+export function downloadProgress(gameId: string, gameProgress: any, ev: React.MouseEvent) {
+  ev.preventDefault()
+  downloadFile({
+    data: JSON.stringify(gameProgress, null, 2),
+    fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
+    fileType: 'text/json',
+  })
+}
 
 /** Pop-up to delete game progress.
  *
@@ -20,23 +29,13 @@ export function ErasePopup ({handleClose}) {
   const gameProgress = useSelector(selectProgress(gameId))
   const dispatch = useAppDispatch()
 
-  /** Download the current progress (i.e. what's saved in the browser store) */
-  const downloadProgress = (e) => {
-    e.preventDefault()
-    downloadFile({
-      data: JSON.stringify(gameProgress, null, 2),
-      fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
-      fileType: 'text/json',
-    })
-  }
-
   const eraseProgress = () => {
     dispatch(deleteProgress({game: gameId}))
     handleClose()
   }
 
-  const downloadAndErase = (e) => {
-    downloadProgress(e)
+  const downloadAndErase = (ev) => {
+    downloadProgress(gameId, gameProgress, ev)
     eraseProgress()
   }
 

client/src/components/welcome.css

@@ -1,189 +0,0 @@
-
-/* svg .world-circle {
-  fill: var(--clr-primary)
-} */
-
-.welcome {
-  height: 100%;
-  flex: 1;
-  min-height: 0;
-  display: flex;
-}
-
-.welcome.mobile .column {
-  width: 100%;
-}
-
-.app-content {
-  height: 100%
-}
-
-.welcome .column {
-  height: 100%;
-  overflow: auto;
-  position: relative;
-  scroll-behavior: smooth;
-}
-
-.welcome-text {
-  padding-left: 20px;
-  padding-right: 20px;
-  padding-bottom: 20px;
-}
-
-i {
-  font-style: italic;
-}
-
-h1 {
-  font-size: 2em;
-  margin: .67em 0;
-}
-
-h2 {
-  font-size: 1.5em;
-}
-
-h3 {
-  font-size: 1.3em;
-}
-
-h4 {
-  font-size: 1.1em;
-  font-style: italic;
-}
-
-h5, h6 {
-  font-size: 1em;
-  font-style: italic;
-}
-
-/******************/
-/* Privacy Button */
-/******************/
-
-.privacy {
-  width: 40px;
-  height: 40px;
-  font-size: 25px;
-  border-radius: 20px;
-  position: fixed;
-  right: 10px;
-  bottom: 10px;
-  display: flex;
-  align-items:center;
-  justify-content:center;
-  color: #aaa;
-  background-color: #eee;
-  cursor: pointer;
-}
-
-.privacy p {
-  position: absolute;
-  color: #888;
-  bottom: 1.5px;
-  font-size: 6px;
-}
-
-.privacy .p1 {
-  transform: rotate(50deg);
-  left: 1.5px;
-}
-
-.privacy .p2 {
-  transform: rotate(-50deg);
-  right: 1.5px;
-}
-
-/*****************/
-/* Privacy Popup */
-/*****************/
-
-.modal-wrapper {
-  position: fixed;
-  top: 0;
-  right: 0;
-  bottom: 0;
-  left: 0;
-  padding: 0;
-}
-
-.modal-backdrop {
-  position: fixed;
-  top: 0;
-  right: 0;
-  bottom: 0;
-  left: 0;
-  background: rgba(0, 0, 0, 0.25);
-  z-index: 2;
-}
-
-.modal h2 {
-  text-align: center;
-}
-
-.modal {
-  position: absolute;
-  top: 50%;
-  left: 50%;
-  transform: translate(-50%, -50%);
-  min-width: max(50%, 300px);
-  max-width: 60ch;
-  max-height: 80%;
-  overflow: scroll;
-  background: #fff;
-  z-index: 3;
-  padding: 2em;
-  border-radius: 1em;
-  text-align: left;
-  color: var(--vscode-breadcrumb-foreground);
-}
-
-.modal input[type="text"] {
-  width: 100%;
-}
-
-.modal .form-error {
-  color: #a00;
-  font-weight: bold;
-}
-
-.modal input[type="submit"] {
-  border: none;
-  color: var(--vscode-button-foreground);
-  background: var(--vscode-button-background);
-  cursor: pointer;
-  padding: .5em 1em;
-  border-radius: .2em;
-  display: block;
-  margin: 1em auto;
-}
-
-.modal-close {
-  float: right;
-  scale: 2;
-  color: var(--vscode-breadcrumb-foreground);
-  cursor: pointer;
-}
-
-.modal-close:hover {
-  float: right;
-  scale: 2;
-  color: var(--vscode-breadcrumb-focusForeground);
-}
-
-.modal table {
-  width: 100%;
-}
-
-.modal a.download-link {
-  cursor: pointer;
-  font-style: italic;
-  text-decoration: underline dotted;
-
-}
-
-.mobile-nav .svg-inline--fa {
-  margin-left: 0.3rem;
-  margin-right: 0.3rem;
-}

client/src/components/welcome.tsx

@@ -1,13 +1,13 @@
 import * as React from 'react'
-import { useState, useEffect } from 'react'
+import { useEffect } from 'react'
 import Split from 'react-split'
 import { Box, CircularProgress } from '@mui/material'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faGlobe, faArrowRight, faArrowLeft } from '@fortawesome/free-solid-svg-icons'
+import { faArrowRight } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
-import { useAppDispatch } from '../hooks'
-import { changedOpenedIntro } from '../state/progress'
+import { useAppDispatch, useAppSelector } from '../hooks'
+import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
 import { Button } from './button'
 import { MobileContext } from './infoview/context'
@@ -19,14 +19,14 @@ import { RulesHelpPopup } from './popup/rules_help'
 import { UploadPopup } from './popup/upload'
 import { WorldTreePanel } from './world_tree'
 
-import './welcome.css'
+import '../css/welcome.css'
 import { WelcomeAppBar } from './app_bar'
 import { Hint } from './hints'
 
 
-/** The panel showing the game's introduction text */
-function IntroductionPanel({introduction}: {introduction: string}) {
-  const {mobile, setPageNumber} = React.useContext(MobileContext)
+/** the panel showing the game's introduction text */
+function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) {
+  const {mobile} = React.useContext(MobileContext)
   const gameId = React.useContext(GameIdContext)
   const dispatch = useAppDispatch()
 
@@ -46,11 +46,6 @@ function IntroductionPanel({introduction}: {introduction: string}) {
         : <></>
       ))}
     </div>
-    {/* <Typography variant="body1" component="div" className="welcome-text">
-          <h1>{title}</h1>
-          <Markdown>{introduction}</Markdown>
-        </Typography>
-    */}
     {mobile &&
       <div className="button-row">
         <Button className="btn" to=""
@@ -65,34 +60,32 @@ function IntroductionPanel({introduction}: {introduction: string}) {
   </div>
 }
 
-/** main page of the game showing amoung others the tree of worlds/levels */
+/** main page of the game showing among others the tree of worlds/levels */
 function Welcome() {
   const gameId = React.useContext(GameIdContext)
-  const {mobile, pageNumber, setPageNumber} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(MobileContext)
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
-  // impressum pop-up
+  // For mobile only
+  const openedIntro = useAppSelector(selectOpenedIntro(gameId))
+  const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0)
+
+  // pop-ups
+  const [eraseMenu, setEraseMenu] = React.useState(false)
   const [impressum, setImpressum] = React.useState(false)
-  const [rulesHelp, setRulesHelp] = React.useState(false)
-
-  function closeImpressum() {setImpressum(false)}
-  function toggleImpressum() {setImpressum(!impressum)}
-  function closeRulesHelp() {setRulesHelp(false)}
-
   const [info, setInfo] = React.useState(false)
-  function closeInfo() {setInfo(false)}
-  function toggleInfo() {setInfo(!impressum)}
-
-
-  /* state variables to toggle the pop-up menus */
-  const [eraseMenu, setEraseMenu] = React.useState(false);
-  const openEraseMenu = () => setEraseMenu(true);
-  const closeEraseMenu = () => setEraseMenu(false);
-  const [uploadMenu, setUploadMenu] = React.useState(false);
-  const openUploadMenu = () => setUploadMenu(true);
-  const closeUploadMenu = () => setUploadMenu(false);
-
+  const [rulesHelp, setRulesHelp] = React.useState(false)
+  const [uploadMenu, setUploadMenu] = React.useState(false)
+  function closeEraseMenu()   {setEraseMenu(false)}
+  function closeImpressum()   {setImpressum(false)}
+  function closeInfo()        {setInfo(false)}
+  function closeRulesHelp()   {setRulesHelp(false)}
+  function closeUploadMenu()  {setUploadMenu(false)}
+  function toggleEraseMenu()  {setEraseMenu(!eraseMenu)}
+  function toggleImpressum()  {setImpressum(!impressum)}
+  function toggleInfo()       {setInfo(!info)}
+  function toggleUploadMenu() {setUploadMenu(!uploadMenu)}
 
   // set the window title
   useEffect(() => {
@@ -106,23 +99,26 @@ function Welcome() {
       <CircularProgress />
     </Box>
   : <>
-    <WelcomeAppBar gameInfo={gameInfo.data} toggleImpressum={toggleImpressum} openEraseMenu={openEraseMenu}
-      openUploadMenu={openUploadMenu} toggleInfo={toggleInfo} />
+    <WelcomeAppBar pageNumber={pageNumber} setPageNumber={setPageNumber} gameInfo={gameInfo.data} toggleImpressum={toggleImpressum}
+      toggleEraseMenu={toggleEraseMenu} toggleUploadMenu={toggleUploadMenu}
+      toggleInfo={toggleInfo} />
     <div className="app-content">
       { mobile ?
           <div className="welcome mobile">
             {(pageNumber == 0 ?
-              <IntroductionPanel introduction={gameInfo.data?.introduction} />
+              <IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
             : pageNumber == 1 ?
-              <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize} rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
+              <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
+                rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
             :
               <InventoryPanel levelInfo={inventory?.data} />
             )}
           </div>
         :
           <Split className="welcome" minSize={0} snapOffset={200}  sizes={[25, 50, 25]}>
-            <IntroductionPanel introduction={gameInfo.data?.introduction} />
-            <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize} rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
+            <IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
+            <WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
+              rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
             <InventoryPanel levelInfo={inventory?.data} />
           </Split>
       }

client/src/components/world_tree.css

@@ -1,117 +0,0 @@
-svg .world-title-wrapper, svg .level-title-wrapper div {
-  overflow: visible;
-}
-
-svg .world-title-wrapper div, svg .level-title-wrapper div {
-  width: 100%;
-  height: 100%;
-}
-
-svg .world-title-wrapper div, svg .level-title-wrapper div {
-  display: flex;
-  align-items:center;
-  justify-content:center;
-  overflow: visible;
-
-}
-
-svg .world-title, svg .level-title {
-  color: white;
-  margin: 0;
-  padding: 0;
-  text-align: center;
-}
-
-svg .world-title {
-  font-weight: 700;
-}
-
-svg .level-title {
-  font-weight: 400;
-  opacity: 0;
-  transition: opacity .3s;
-}
-
-svg .level:hover .level-title {
-  opacity: 1;
-}
-
-svg .disabled {
-  cursor: default;
-}
-
-.world-selection {
-  display: block;
-  margin-left: auto;
-  margin-right: auto;
-  margin-top: 2em;
-  max-width: 100%;
-}
-
-.world-selection-menu {
-  position: absolute;
-  right: 1em;
-  top: 1em;
-  /* margin: 1em; */
-  /* border: 1px solid var(--clr-primary); */
-  border: 1px solid var(--clr-primary);
-  background-color: #fff;
-  border-radius: .5em;
-  filter: drop-shadow(4px 4px 5px rgba(0,0,0,0.5));
-}
-
-.world-selection-menu .btn, .welcome .btn {
-  min-width: 5em;
-  text-align: center;
-  margin-left: .4em;
-  margin-right: .4em;
-  margin-bottom: .2em;
-}
-
-.world-selection-menu .slider-wrap {
-  display: flex;
-  flex-direction: column;
-  /* width: 100%; */
-  height: 7em;
-  /* min-width: 16em; */
-  padding: .5em 1em 1.3em 1em;
-  margin-left: auto;
-  margin-right: auto;
-}
-
-.difficulty-label {
-  /* font-size: 0.875em; */
-  padding-bottom: 1.2em;
-}
-
-/* Test for mobile `title`s */
-/* @media (pointer: coarse), (hover: none) {
-  [title] {
-    position: relative;
-    display: inline-flex;
-    justify-content: center;
-  }
-  [title]:focus::after {
-    content: attr(title);
-    position: absolute;
-    top: 90%;
-    color: #000;
-    background-color: #fff;
-    border: 1px solid;
-    width: fit-content;
-    padding: 3px;
-  }
-} */
-
-.world-label {
-  /* border: 2px solid purple; */
-  padding: .2em;
-  border-radius: .5em;
-}
-
-.world-selection-menu .helpButton {
-  position: absolute;
-  right: .5em;
-  top: .5em;
-  color: var(--clr-primary);
-}

client/src/components/world_tree.tsx

@@ -15,7 +15,7 @@ import { useAppDispatch } from '../hooks'
 import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
 import { store } from '../state/store'
 
-import './world_tree.css'
+import '../css/world_tree.css'
 
 // Settings for the world tree
 cytoscape.use( klay )