stuff

client/src/components/infoview/goals.tsx

@@ -1,13 +1,17 @@
-/* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/goals.tsx */
+/**
+ * @fileOverview
+ *
+ * Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/goals.tsx
+*/
 
 import * as React from 'react'
-import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
 import { InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api'
-import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips';
 import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
-import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpc_api';
+import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
+import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips';
 import { InputModeContext } from './context';
+import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpc_api';
 
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */

client/src/components/level.tsx

@@ -83,7 +83,6 @@ function PlayableLevel({worldId, levelId}) {
 
   const theme = useTheme();
 
-
   useEffect(() => {
     // Scroll to top when loading a new level
     // TODO: Thats the wrong behaviour probably
@@ -416,7 +415,9 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCo
       editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
       editor.setModel(model)
       if (initialSelections) {
-        editor.setSelections(initialSelections)
+        console.debug("Initial Selection: ", initialSelections)
+        // BUG: Somehow I get an `invalid arguments` bug here
+        // editor.setSelections(initialSelections)
       }
 
       infoviewApi.serverRestarted(leanClient.initializeResult)

client/src/components/privacy_policy.tsx

@@ -1,61 +1,62 @@
+/**
+ * @fileOverview The impressum/privacy policy
+*/
 import { faShield } from '@fortawesome/free-solid-svg-icons';
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome';
 import * as React from 'react'
 
-function PrivacyPolicyPopup ({handleClose}) {
+/** Pop-up that is displayed when opening the privacy policy.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+function PrivacyPolicyPopup (handleClose) {
   return <div className="modal-wrapper">
   <div className="modal-backdrop" onClick={handleClose} />
   <div className="modal">
     <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
     <h2>Privacy Policy &amp; Impressum</h2>
-
+    <p>
-    <p>Our server collects metadata (such as IP address, browser, operating system)
+      Our server collects metadata (such as IP address, browser, operating system)
-    and the data that the user enters into the editor. The data is used to
+      and the data that the user enters into the editor. The data is used to
-    compute the Lean output and display it to the user. The information will be stored
+      compute the Lean output and display it to the user. The information will be stored
-    as long as the user stays on our website and will be deleted immediately afterwards.
+      as long as the user stays on our website and will be deleted immediately afterwards.
-    We keep logs to improve our software, but the contained data is anonymized.</p>
+      We keep logs to improve our software, but the contained data is anonymized.
-
+    </p>
-    <p>We do not use cookies, but your game progress is stored in the browser
+    <p>
+      We do not use cookies, but your game progress is stored in the browser
       as site data. Your game progress is not saved on the server; if you delete
       your browser storage, it is completely gone.
     </p>
-
     <p>Our server is located in Germany.</p>
-
+    <p>
-    <p><strong>Contact information:</strong><br />
+      <strong>Contact information:</strong><br />
       Jon Eugster<br />
       Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
       Universitätsstr. 1<br />
       40225 Düsseldorf<br />
       Germany<br />
+      +49 211 81-12173<br />
       <a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Contact Details</a>
-
     </p>
   </div>
 </div>
 }
 
 const PrivacyPolicy: React.FC = () => {
-  const [open, setOpen] = React.useState(false);
+  const [open, setOpen] = React.useState(false)
-  const handleOpen = () => setOpen(true);
+  const handleOpen = () => setOpen(true)
-  const handleClose = () => setOpen(false);
+  const handleClose = () => setOpen(false)
-
   return (
     <span>
-          <div className="privacy" onClick={handleOpen} title="Privacy Policy &amp; Impressum">
+      <div className="privacy" onClick={handleOpen} title="Privacy Policy &amp; Impressum">
-            <FontAwesomeIcon icon={faShield} />
+        <FontAwesomeIcon icon={faShield} />
-            <p className="p1">legal</p>
+        <p className="p1">legal</p>
-            <p className="p2">notes</p>
+        <p className="p2">notes</p>
-          </div>
+      </div>
-      {open?
+      {open ? <PrivacyPolicyPopup handleClose={handleClose} /> : null}
-        <PrivacyPolicyPopup handleClose={handleClose} />: null}
     </span>
   )
 }
 
-// export default PrivacyPolicy
+export {PrivacyPolicy, PrivacyPolicyPopup}
-
-export {
-  PrivacyPolicy,
-  PrivacyPolicyPopup,
-}

client/src/components/welcome.css

@@ -196,18 +196,6 @@ svg .world-title {
   width: 100%;
 }
 
-.game-menu {
-  padding: .5em;
-}
-
-.game-menu .btn {
-  min-width: 5em;
-  text-align: center;
-  margin-left: .4em;
-  margin-right: .4em;
-  margin-bottom: .2em;
-}
-
 .modal a.download-link {
   cursor: pointer;
   font-style: italic;

client/src/components/welcome.tsx

@@ -12,7 +12,7 @@ import { GameIdContext } from '../app';
 import { selectCompleted } from '../state/progress';
 import { useGetGameInfoQuery } from '../state/api';
 import Markdown from './markdown';
-import GameMenu from './game_menu';
+import WorldSelectionMenu from './world_selection_menu';
 import {PrivacyPolicy} from './privacy_policy';
 
 cytoscape.use( klay );
@@ -104,7 +104,7 @@ function Welcome() {
         </Typography>
       </div>
       <div className="column">
-        <GameMenu />
+        <WorldSelectionMenu />
         <Box textAlign='center' sx={{ m: 5 }}>
           <svg xmlns="http://www.w3.org/2000/svg" xmlnsXlink="http://www.w3.org/1999/xlink"
               viewBox={bounds ? `${s*bounds.x1 - padding} ${s*bounds.y1 - padding} ${s*bounds.x2 - s*bounds.x1 + 2 * padding} ${s*bounds.y2 - s*bounds.y1 + 2 * padding}` : ''}>

client/src/components/world_selection_menu.css

@@ -0,0 +1,11 @@
+.world-selection-menu {
+  padding: .5em;
+}
+
+.world-selection-menu .btn {
+  min-width: 5em;
+  text-align: center;
+  margin-left: .4em;
+  margin-right: .4em;
+  margin-bottom: .2em;
+}

client/src/components/world_selection_menu.tsx

@@ -1,14 +1,27 @@
+/**
+ * @fileOverview Define the menu displayed with the tree of worlds on the welcome page
+*/
 import * as React from 'react'
 import { useStore, useSelector } from 'react-redux';
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faDownload, faUpload, faEraser } from '@fortawesome/free-solid-svg-icons'
 
+import './world_selection_menu.css'
+
 import { Button } from './button'
 import { GameIdContext } from '../app';
 import { useAppDispatch, useAppSelector } from '../hooks';
 import { deleteProgress, selectProgress, loadProgress, GameProgressState } from '../state/progress';
 
-const downloadFile = ({ data, fileName, fileType }) => {
+/** Only to specify the types for `downloadFile` */
+interface downloadFileParam {
+  data: string
+  fileName: string
+  fileType: string
+}
+
+/** Download a file containing `data` */
+const downloadFile = ({ data, fileName, fileType } : downloadFileParam) => {
   const blob = new Blob([data], { type: fileType })
   const a = document.createElement('a')
   a.download = fileName
@@ -22,25 +35,25 @@ const downloadFile = ({ data, fileName, fileType }) => {
   a.remove()
 }
 
-function GameMenu() {
+/** 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()
 
+  /* 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({
@@ -48,29 +61,24 @@ function GameMenu() {
       fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
       fileType: 'text/json',
     })
-  };
+  }
 
   const handleFileChange = (e) => {
     if (e.target.files) {
-      setFile(e.target.files[0]);
+      setFile(e.target.files[0])
     }
+  }
 
-  };
+  /** Upload progress from a  */
-
   const uploadProgress = (e) => {
-    if (!file) {
+    if (!file) {return}
-      return;
+    const fileReader = new FileReader()
-    }
+    fileReader.readAsText(file, "UTF-8")
-
-    const fileReader = new FileReader();
-    fileReader.readAsText(file, "UTF-8");
     fileReader.onload = (e) => {
-      const data = JSON.parse(e.target.result.toString()) as GameProgressState;
+      const data = JSON.parse(e.target.result.toString()) as GameProgressState
-      console.debug("Json Data", data);
+      console.debug("Json Data", data)
-
       dispatch(loadProgress({game: gameId, data: data}))
     }
-
     closeUploadMenu()
   }
 
@@ -84,46 +92,44 @@ function GameMenu() {
     eraseProgress()
   }
 
-  return <nav className="game-menu">
+  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>
-
     {eraseMenu?
       <div className="modal-wrapper">
-      <div className="modal-backdrop" onClick={closeEraseMenu} />
+        <div className="modal-backdrop" onClick={closeEraseMenu} />
-      <div className="modal">
+        <div className="modal">
-        <div className="codicon codicon-close modal-close" onClick={closeEraseMenu}></div>
+          <div className="codicon codicon-close modal-close" onClick={closeEraseMenu}></div>
-        <h2>Delete Progress?</h2>
+          <h2>Delete Progress?</h2>
 
-        <p>Do you want to delete your saved progress irreversibly?</p>
+          <p>Do you want to delete your saved progress irreversibly?</p>
-        <p>(This only affects your saved proofs, no levels are ever locked.
+          <p>(This only affects your saved proofs, no levels are ever locked.
-          Saves from other games are not deleted.)</p>
+            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}
 
+          <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-backdrop" onClick={closeUploadMenu} />
-      <div className="modal">
+        <div className="modal">
-        <div className="codicon codicon-close modal-close" onClick={closeUploadMenu}></div>
+          <div className="codicon codicon-close modal-close" onClick={closeUploadMenu}></div>
-        <h2>Upload Saved Progress</h2>
+          <h2>Upload Saved Progress</h2>
 
-        <p>Select a JSON file with the saved game progress to load your progress.</p>
+          <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!
+          <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>
+            Consider <a className="download-link" onClick={downloadProgress} >downloading your current progress</a> first!</p>
 
-        <input type="file" onChange={handleFileChange}/>
+          <input type="file" onChange={handleFileChange}/>
 
-        <Button to="" onClick={uploadProgress}>Load selected file</Button>
+          <Button to="" onClick={uploadProgress}>Load selected file</Button>
-      </div>
+        </div>
-    </div> : null}
+      </div> : null}
   </nav>
 }
 
-export default GameMenu
+export default WorldSelectionMenu