cleanup: popups

client/src/app.tsx

@@ -9,14 +9,14 @@ import '@fontsource/roboto/700.css';
 
 import './css/reset.css';
 import './css/app.css';
-import { PageContext, PopupContext, PreferencesContext} from './components/infoview/context';
+import { PageContext, PreferencesContext} from './components/infoview/context';
 import UsePreferences from "./state/hooks/use_preferences"
 import i18n from './i18n';
 import { Navigation } from './components/navigation';
 import { useSelector } from 'react-redux';
-import { changeTypewriterMode, selectTypewriterMode } from './state/progress';
+import { changeTypewriterMode, selectOpenedIntro, selectTypewriterMode } from './state/progress';
 import { useAppDispatch } from './hooks';
-import { Popup } from './components/popup/popup';
+import { Popup, PopupContext } from './components/popup/popup';
 
 export const GameIdContext = React.createContext<{
   gameId: string,
@@ -40,6 +40,16 @@ function App() {
   const [page, setPage] = useState(0)
   const [popupContent, setPopupContent] = useState(null)
 
+
+  const openedIntro = useSelector(selectOpenedIntro(gameId))
+
+  useEffect(() => {
+    if (openedIntro && !worldId && page == 0) {
+      setPage(1)
+    }
+  }, [openedIntro])
+
+
   useEffect(() => {
     i18n.changeLanguage(language)
   }, [language])

client/src/components/level.tsx

@@ -49,7 +49,7 @@ import { IConnectionProvider } from 'monaco-languageclient'
 import { monacoSetup } from 'lean4web/client/src/monacoSetup'
 import { onigasmH } from 'onigasm/lib/onigasmH'
 import { isLastStepWithErrors, lastStepHasErrors } from './infoview/goals'
-import { InfoPopup } from './popup/game_info'
+import { InfoPopup } from './popup/info'
 import { PreferencesPopup } from './popup/preferences'
 import { useTranslation } from 'react-i18next'
 import i18next from 'i18next'

client/src/components/navigation.tsx

@@ -11,6 +11,8 @@ import { downloadProgress } from './popup/erase'
 import { useTranslation } from 'react-i18next'
 import '../css/navigation.css'
 import { PopupContext } from './popup/popup'
+import { useSelector } from 'react-redux'
+import { selectProgress } from '../state/progress'
 
 /** SVG github icon */
 function GithubIcon () {
@@ -41,15 +43,29 @@ const NavigationContext = createContext<{
   setNavOpen: React.Dispatch<React.SetStateAction<boolean>>
 }>({navOpen: false, setNavOpen: () => {}})
 
+/** Content of the navigation during game selection. */
+function NavigationLandingPage () {
+  return <div className="nav-content">
+    <div className="nav-title-left"></div>
+    <div className="nav-title-middle"></div>
+    <div className="nav-title-right"></div>
+  </div>
+}
 
 /** Content of the navigation on Desktop during world selection. */
 function DesktopNavigationOverview () {
   const { t } = useTranslation()
-  const {gameId} = useContext(GameIdContext)
+  const { gameId } = useContext(GameIdContext)
+  const { setPopupContent } = useContext(PopupContext)
   const gameInfo = useGetGameInfoQuery({game: gameId})
 
   return <div className="nav-content">
-    <div className="nav-title-left"></div>
+    <div className="nav-title-left">
+      <NavButton
+        text={t("Rules")}
+        onClick={() => {setPopupContent("rules")}}
+        inverted={true} />
+    </div>
     <div className="nav-title-middle">
       <span className="nav-title">{t(gameInfo.data?.title, {ns: gameId})}</span>
     </div>
@@ -61,9 +77,15 @@ function DesktopNavigationOverview () {
 function MobileNavigationOverview () {
   const { t } = useTranslation()
   const {page, setPage} = useContext(PageContext)
+  const { setPopupContent } = useContext(PopupContext)
 
   return <div className="nav-content">
-    <div className="nav-title-left"></div>
+    <div className="nav-title-left">
+      <NavButton
+        text={t("Rules")}
+        onClick={() => {setPopupContent("rules")}}
+        inverted={true} />
+    </div>
     <div className="nav-title-middle">
       <span className="nav-title">
       </span>
@@ -88,15 +110,6 @@ function MobileNavigationOverview () {
   </div>
 }
 
-/** Content of the navigation during game selection. */
-function NavigationLandingPage () {
-  return <div className="nav-content">
-    <div className="nav-title-left"></div>
-    <div className="nav-title-middle"></div>
-    <div className="nav-title-right"></div>
-  </div>
-}
-
 /** Content of the navigation on Desktop in a level. */
 function DesktopNavigationLevel () {
   const { t } = useTranslation()
@@ -201,6 +214,8 @@ export function Navigation () {
   const { gameId, worldId } = useContext(GameIdContext)
   const { mobile } = useContext(PreferencesContext)
   const { setPopupContent } = useContext(PopupContext)
+  const gameProgress = useSelector(selectProgress(gameId))
+
 
   const [navOpen, setNavOpen] = useState(false)
   function toggleNav () {setNavOpen(!navOpen)}
@@ -246,7 +261,7 @@ export function Navigation () {
             <NavButton
               icon={faDownload}
               text={t("Download")}
-              onClick={() => {downloadProgress(gameId)}}
+              onClick={() => {downloadProgress(gameId, gameProgress)}}
               inverted={true} />
             <NavButton
               icon={faUpload}

client/src/components/popup/erase.tsx

@@ -10,8 +10,7 @@ import { useContext } from 'react'
 import { PopupContext } from './popup'
 
 /** download the current progress (i.e. what's saved in the browser store) */
-export function downloadProgress(gameId: string) {
-  const gameProgress = useSelector(selectProgress(gameId))
+export function downloadProgress(gameId: string, gameProgress) {
 
   // ev.preventDefault()
   downloadFile({
@@ -33,14 +32,15 @@ export function ErasePopup () {
   const dispatch = useAppDispatch()
   const { setPopupContent } = useContext(PopupContext)
 
-  const eraseProgress = () => {
+  const eraseProgress = (ev) => {
     dispatch(deleteProgress({game: gameId}))
     setPopupContent(null)
+    ev.preventDefault() // TODO: this is a hack to prevent the buttons below from opening a link
   }
 
   const downloadAndErase = (ev) => {
-    downloadProgress(gameId)
-    eraseProgress()
+    downloadProgress(gameId, gameProgress)
+    eraseProgress(ev)
   }
 
   return <>
@@ -54,6 +54,6 @@ export function ErasePopup () {
     </Trans>
     <Button onClick={eraseProgress} to="">{t("Delete")}</Button>
     <Button onClick={downloadAndErase} to="">{t("Download & Delete")}</Button>
-    <Button onClick={() => {setPopupContent(null)}} to="">{t("Cancel")}</Button>
+    <Button onClick={(ev) => {setPopupContent(null); ev.preventDefault()}} to="">{t("Cancel")}</Button>
   </>
 }

client/src/components/popup/info.tsx

@@ -1,6 +1,3 @@
-/**
- * @fileOverview
-*/
 import * as React from 'react'
 import { Typography } from '@mui/material'
 import Markdown from '../markdown'

client/src/components/popup/popup.tsx

@@ -1,11 +1,13 @@
 import * as React from 'react'
 import { useContext } from 'react'
-import { PrivacyPolicyPopup } from './privacy_policy'
+import { PrivacyPolicyPopup } from './privacy'
 import { ImpressumPopup } from './impressum'
-import { InfoPopup } from './game_info'
+import { InfoPopup } from './info'
 import { ErasePopup } from './erase'
 import { PreferencesPopup } from './preferences'
 import { UploadPopup } from './upload'
+import { RulesPopup } from './rules'
+import '../../css/popup.css'
 
 /** The context which manages if a popup is shown.
  * If `popupContent` is `null`, the popup is closed.
@@ -30,6 +32,7 @@ export const Popups = {
   "info": <InfoPopup />,
   "preferences": <PreferencesPopup />,
   "privacy": <PrivacyPolicyPopup />,
+  "rules": <RulesPopup />,
   "upload": <UploadPopup />,
 }
 

client/src/components/popup/rules.tsx

@@ -0,0 +1,88 @@
+import { Box, Slider } from '@mui/material'
+import * as React from 'react'
+import { Trans, useTranslation } from 'react-i18next'
+import { GameIdContext } from '../../app'
+import { changedDifficulty, selectDifficulty } from '../../state/progress'
+import { useSelector } from 'react-redux'
+import { useContext } from 'react'
+import { useAppDispatch } from '../../hooks'
+
+/** Pop-up that is displayed when opening the help explaining the game rules.
+ *
+ */
+export function RulesPopup () {
+  const { t } = useTranslation()
+  const { gameId } = useContext(GameIdContext)
+  const difficulty = useSelector(selectDifficulty(gameId))
+  const dispatch = useAppDispatch()
+
+  function label(x : number) {
+    return x == 0 ? t("none") : x == 1 ? t("relaxed") : t("regular")
+  }
+
+  return <>
+    <h2>{t("Game Rules")}</h2>
+
+    {/* <span className="difficulty-label">{t("Rules")}
+        <FontAwesomeIcon icon={rulesHelp ? faXmark : faCircleQuestion} className='helpButton' onClick={() => (setRulesHelp(!rulesHelp))}/>
+      </span> */}
+      <Box className="slider-wrapper">
+      <Slider
+        orientation="horizontal"
+        title={t("Game Rules")}
+        min={0} max={2}
+        aria-label={t("Game Rules")}
+        value={difficulty}
+        marks={[
+          {value: 0, label: label(0)},
+          {value: 1, label: label(1)},
+          {value: 2, label: label(2)}
+        ]}
+        valueLabelFormat={label}
+        getAriaValueText={label}
+        valueLabelDisplay="off"
+        onChange={(ev, val: number) => {
+          dispatch(changedDifficulty({game: gameId, difficulty: val}))
+        }}
+        />
+        </Box>
+    <Trans>
+      <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>
+    </Trans>
+    <table>
+      <thead>
+        <tr>
+          <th scope="col"></th>
+          <th scope="col">{t("levels")}</th>
+          <th scope="col">{t("tactics")}</th>
+        </tr>
+      </thead>
+      <tbody>
+        <tr>
+          <th scope="row">{t("regular")}</th>
+          <td>🔐</td>
+          <td>🔐</td>
+        </tr>
+        <tr>
+          <th scope="row">{t("relaxed")}</th>
+          <td>🔓</td>
+          <td>🔐</td>
+        </tr>
+        <tr>
+          <th scope="row">{t("none")}</th>
+          <td>🔓</td>
+          <td>🔓</td>
+        </tr>
+      </tbody>
+    </table>
+  </>
+}

client/src/components/popup/rules_help.tsx

@@ -1,60 +0,0 @@
-/**
- * @fileOverview
-*/
-import * as React from 'react'
-import { Trans, useTranslation } from 'react-i18next'
-
-/** 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}) {
-  const { t } = useTranslation()
-
-  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>{t("Game Rules")}</h2>
-    <Trans>
-      <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>
-    </Trans>
-    <table>
-      <thead>
-        <tr>
-          <th scope="col"></th>
-          <th scope="col">{t("levels")}</th>
-          <th scope="col">{t("tactics")}</th>
-        </tr>
-      </thead>
-      <tbody>
-        <tr>
-          <th scope="row">{t("regular")}</th>
-          <td>🔐</td>
-          <td>🔐</td>
-        </tr>
-        <tr>
-          <th scope="row">{t("relaxed")}</th>
-          <td>🔓</td>
-          <td>🔐</td>
-        </tr>
-        <tr>
-          <th scope="row">{t("none")}</th>
-          <td>🔓</td>
-          <td>🔓</td>
-        </tr>
-      </tbody>
-    </table>
-  </div>
-</div>
-}

client/src/components/welcome.tsx

@@ -13,9 +13,8 @@ import { Button } from './button'
 import { PageContext, PreferencesContext } from './infoview/context'
 import { InventoryPanel } from './inventory'
 import { ErasePopup } from './popup/erase'
-import { InfoPopup } from './popup/game_info'
-import { PrivacyPolicyPopup } from './popup/privacy_policy'
-import { RulesHelpPopup } from './popup/rules_help'
+import { InfoPopup } from './popup/info'
+import { PrivacyPolicyPopup } from './popup/privacy'
 import { UploadPopup } from './popup/upload'
 import { PreferencesPopup} from "./popup/preferences"
 import { WorldTreePanel } from './world_tree'

client/src/components/world_tree.tsx

@@ -360,7 +360,7 @@ export function WorldTreePanel({worlds, worldSize, rulesHelp, setRulesHelp}:
   let dx = bounds ? s*(bounds.x2 - bounds.x1) + 2*padding : null
 
   return <div className="column">
-      <WorldSelectionMenu rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
+      {/* <WorldSelectionMenu rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} /> */}
       <svg xmlns="http://www.w3.org/2000/svg" xmlnsXlink="http://www.w3.org/1999/xlink"
           width={bounds ? `${ds * dx}` : ''}
           viewBox={bounds ? `${s*bounds.x1 - padding} ${s*bounds.y1 - padding} ${dx} ${s*(bounds.y2 - bounds.y1) + 2 * padding}` : ''}

client/src/css/popup.css

@@ -0,0 +1,7 @@
+
+/* For the "Rules" popup. */
+.slider-wrapper {
+  padding-left: 2rem;
+  padding-right: 2rem;
+  padding-top: 1rem;
+}

client/src/state/progress.ts

@@ -184,7 +184,7 @@ export function selectCompleted(game: string, world: string, level: number) {
 /** return progress for the current game if it exists */
 export function selectProgress(game: string) {
   return (state) => {
-    return state.progress.games[game.toLowerCase()] ?? null
+    return state.progress.games[game?.toLowerCase()] ?? null
   }
 }
 
@@ -198,7 +198,7 @@ export function selectDifficulty(game: string) {
 /** return whether the intro has been read */
 export function selectOpenedIntro(game: string) {
   return (state) => {
-    return state.progress.games[game.toLowerCase()]?.openedIntro
+    return state.progress.games[game?.toLowerCase()]?.openedIntro
   }
 }