reorganise popups

client/src/components/app_bar.tsx

@@ -8,7 +8,7 @@ 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 './privacy_policy'
+import { PrivacyPolicyPopup } from './popup/privacy_policy'
 import { WorldSelectionMenu, downloadFile } from './world_tree'
 
 /** navigation to switch between pages on mobile */

client/src/components/landing_page.tsx

@@ -11,7 +11,7 @@ import coverRobo from '../assets/covers/formaloversum.png'
 import bgImage from '../assets/bg.jpg'
 
 import Markdown from './markdown';
-import {PrivacyPolicyPopup} from './privacy_policy'
+import {PrivacyPolicyPopup} from './popup/privacy_policy'
 
 const flag = {
   'Dutch': '🇳🇱',

client/src/components/level.tsx

@@ -33,7 +33,7 @@ import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContex
 import { DualEditor } from './infoview/main'
 import { GameHint } from './infoview/rpc_api'
 import { DeletedHints, Hint, Hints } from './hints'
-import { PrivacyPolicyPopup } from './privacy_policy'
+import { PrivacyPolicyPopup } from './popup/privacy_policy'
 
 import '@fontsource/roboto/300.css'
 import '@fontsource/roboto/400.css'

client/src/components/popup/erase.tsx

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

client/src/components/popup/game_info.tsx

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

client/src/components/popup/rules_help.tsx

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

client/src/components/popup/upload.tsx

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

client/src/components/welcome.tsx

@@ -1,27 +1,29 @@
 import * as React from 'react'
 import { useState, useEffect } from 'react'
-import { useSelector } from 'react-redux'
 import Split from 'react-split'
-import { Box, Typography, CircularProgress } from '@mui/material'
+import { Box, CircularProgress } from '@mui/material'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faGlobe, faArrowRight, faArrowLeft } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
 import { useAppDispatch } from '../hooks'
-import { GameProgressState, changedOpenedIntro, deleteProgress, loadProgress, selectOpenedIntro, selectProgress } from '../state/progress'
+import { changedOpenedIntro } from '../state/progress'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
 import { Button } from './button'
 import { MobileContext } from './infoview/context'
 import { InventoryPanel } from './inventory'
-import Markdown from './markdown'
+import { ErasePopup } from './popup/erase'
-import { PrivacyPolicyPopup } from './privacy_policy'
+import { InfoPopup } from './popup/game_info'
+import { PrivacyPolicyPopup } from './popup/privacy_policy'
 import { RulesHelpPopup } from './popup/rules_help'
-import { WorldTreePanel, downloadFile } from './world_tree'
+import { UploadPopup } from './popup/upload'
+import { WorldTreePanel } from './world_tree'
 
 import './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)
@@ -63,117 +65,6 @@ function IntroductionPanel({introduction}: {introduction: string}) {
   </div>
 }
 
-export function InfoPopup ({info, handleClose}: {info: string, handleClose: () => void}) {
-  return <div className="modal-wrapper">
-  <div className="modal-backdrop" onClick={handleClose} />
-  <div className="modal">
-    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <Typography variant="body1" component="div" className="welcome-text">
-      <Markdown>{info}</Markdown>
-    </Typography>
-  </div>
-</div>
-}
-
-
-function ErasePopup ({handleClose}) {
-  const gameId = React.useContext(GameIdContext)
-  const gameProgress = useSelector(selectProgress(gameId))
-  const dispatch = useAppDispatch()
-
-  /** Download the current progress (i.e. what's saved in the browser store) */
-  const downloadProgress = (e) => {
-    e.preventDefault()
-    downloadFile({
-      data: JSON.stringify(gameProgress, null, 2),
-      fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
-      fileType: 'text/json',
-    })
-  }
-
-  const eraseProgress = () => {
-    dispatch(deleteProgress({game: gameId}))
-    handleClose()
-  }
-
-  const downloadAndErase = (e) => {
-    downloadProgress(e)
-    eraseProgress()
-  }
-
-  return <div className="modal-wrapper">
-  <div className="modal-backdrop" onClick={handleClose} />
-  <div className="modal">
-    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h2>Delete Progress?</h2>
-
-    <p>Do you want to delete your saved progress irreversibly?</p>
-    <p>
-      (This deletes your proofs and your collected inventory.
-      Saves from other games are not deleted.)
-    </p>
-
-    <Button onClick={eraseProgress} to="">Delete</Button>
-    <Button onClick={downloadAndErase} to="">Download & Delete</Button>
-    <Button onClick={handleClose} to="">Cancel</Button>
-  </div>
-</div>
-}
-
-function UploadPopup ({handleClose}) {
-  const [file, setFile] = React.useState<File>();
-  const gameId = React.useContext(GameIdContext)
-  const gameProgress = useSelector(selectProgress(gameId))
-  const dispatch = useAppDispatch()
-
-  const handleFileChange = (e) => {
-    if (e.target.files) {
-      setFile(e.target.files[0])
-    }
-  }
-
-  /** Upload progress from a  */
-  const uploadProgress = (e) => {
-    if (!file) {return}
-    const fileReader = new FileReader()
-    fileReader.readAsText(file, "UTF-8")
-    fileReader.onload = (e) => {
-      const data = JSON.parse(e.target.result.toString()) as GameProgressState
-      console.debug("Json Data", data)
-      dispatch(loadProgress({game: gameId, data: data}))
-    }
-    handleClose()
-  }
-
-  /** Download the current progress (i.e. what's saved in the browser store) */
-  const downloadProgress = (e) => {
-    e.preventDefault()
-    downloadFile({
-      data: JSON.stringify(gameProgress, null, 2),
-      fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
-      fileType: 'text/json',
-    })
-  }
-
-
-  return <div className="modal-wrapper">
-  <div className="modal-backdrop" onClick={handleClose} />
-  <div className="modal">
-    <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h2>Upload Saved Progress</h2>
-
-    <p>Select a JSON file with the saved game progress to load your progress.</p>
-
-    <p><b>Warning:</b> This will delete your current game progress!
-      Consider <a className="download-link" onClick={downloadProgress} >downloading your current progress</a> first!</p>
-
-    <input type="file" onChange={handleFileChange}/>
-
-    <Button to="" onClick={uploadProgress}>Load selected file</Button>
-  </div>
-</div>
-}
-
 /** main page of the game showing amoung others the tree of worlds/levels */
 function Welcome() {
   const gameId = React.useContext(GameIdContext)

client/src/components/world_tree.tsx

@@ -8,14 +8,12 @@ import { Slider } from '@mui/material'
 import cytoscape, { LayoutOptions } from 'cytoscape'
 import klay from 'cytoscape-klay'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { faDownload, faUpload, faEraser, faGlobe, faArrowLeft, faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons'
+import { faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
 import { useAppDispatch } from '../hooks'
-import { deleteProgress, selectProgress, loadProgress, GameProgressState,
+import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
-  selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
 import { store } from '../state/store'
-import { Button } from './button'
 
 import './world_tree.css'