diff --git a/client/src/app.css b/client/src/app.css index aa077c0..3dabc1e 100644 --- a/client/src/app.css +++ b/client/src/app.css @@ -125,9 +125,13 @@ em { } .app-content { + height: 100%; flex: 1; + min-height: 0; + display: flex; } + .markdown li ul, .markdown li ol { margin:0 1.5em; } diff --git a/client/src/app.tsx b/client/src/app.tsx index d4605eb..b0ef13c 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -10,6 +10,8 @@ import './reset.css'; import './app.css'; import { MobileContext } from './components/infoview/context'; import { useWindowDimensions } from './window_width'; +import { selectOpenedIntro } from './state/progress'; +import { useSelector } from 'react-redux'; export const GameIdContext = React.createContext(undefined); @@ -22,10 +24,15 @@ function App() { const {width, height} = useWindowDimensions() const [mobile, setMobile] = React.useState(width < 800) + // On mobile, there are multiple pages on the welcome page to switch between + const openedIntro = useSelector(selectOpenedIntro(gameId)) + // On mobile, there are multiple pages to switch between + const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0) + return (
- + diff --git a/client/src/components/app_bar.tsx b/client/src/components/app_bar.tsx new file mode 100644 index 0000000..51838cb --- /dev/null +++ b/client/src/components/app_bar.tsx @@ -0,0 +1,403 @@ +import * as React from 'react' +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, faGlobe, faHome, faArrowRight, faArrowLeft, faXmark, faBars, faCode, faCircleInfo, faTerminal } from '@fortawesome/free-solid-svg-icons' +import { PrivacyPolicyPopup } from './privacy_policy' +import { WorldSelectionMenu, downloadFile } from './world_tree' + +/** navigation to switch between pages on mobile */ +function MobileNav({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: faXmark}[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] + + return <> + {(prevText || prevTitle || prevIcon) && + + } + {(nextText || nextTitle || nextIcon) && + + } + +} + +export function WelcomeAppBar({gameInfo, toggleImpressum, openEraseMenu, openUploadMenu} : { + gameInfo: GameInfo, + toggleImpressum: any, + openEraseMenu: any, + openUploadMenu: 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
+ <> +
+ + + {} + +
+
+ + {mobile ? '' : gameInfo.title} + +
+
+ {mobile && <> + {/* BUTTONS for MOBILE */} + + + } + + + +
+
+ {/* {levelId < gameInfo.data?.worldSize[worldId] && + + } + {levelId > 0 && <> + + } + + */} + + + + + + +
+ +
+ + + +} + +// /** The menu that is shown next to the world selection graph */ +// function WorldSelectionMenu() { +// const [file, setFile] = React.useState(); + +// 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 +// } + + +/** The top-navigation bar */ +export function LevelAppBar({ + isLoading, levelTitle, impressum, toggleImpressum, + pageNumber = undefined, setPageNumber = undefined}) { + const gameId = React.useContext(GameIdContext) + const {worldId, levelId} = React.useContext(WorldLevelIdContext) + const gameInfo = useGetGameInfoQuery({game: gameId}) + + const {mobile} = React.useContext(MobileContext) + + const difficulty = useSelector(selectDifficulty(gameId)) + const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) + + const { commandLineMode, setCommandLineMode } = React.useContext(InputModeContext) + + const [navOpen, setNavOpen] = React.useState(false) + + return
+ {mobile ? + <> + {/* MOBILE VERSION */} +
+ + {levelTitle} + +
+
+ {mobile && pageNumber == 0 ? + + : pageNumber == 1 && + + } + +
+
+ {levelId < gameInfo.data?.worldSize[worldId] && + + } + {levelId > 0 && <> + + } + + + +
+ + : + <> + {/* DESKTOP VERSION */} +
+ + + {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`} + +
+
+ + {levelTitle} + +
+
+ {levelId > 0 && <> + + } + {levelId < gameInfo.data?.worldSize[worldId] ? + + : + + } + + +
+ + } +
+} diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts index 8f0bce7..27fe0bb 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/components/infoview/context.ts @@ -64,10 +64,14 @@ export const ProofStateContext = React.createContext<{ export const MobileContext = React.createContext<{ mobile : boolean, - setMobile: React.Dispatch> + setMobile: React.Dispatch>, + pageNumber: number, + setPageNumber: React.Dispatch> }>({ mobile : false, setMobile: () => {}, + pageNumber: 0, + setPageNumber: () => {} }) export const WorldLevelIdContext = React.createContext<{ diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 0570b0a..f7a2437 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -418,68 +418,70 @@ export function CommandLineInterface(props: { world: string, level: number, data }
- - {proof.length ? -
- {proof.map((step, i) => { - if (i == proof.length - 1 && lastStepErrors) { - // if the last command contains an error, we only display the errors but not the - // entered command as it is still present in the command line. - // TODO: Should not use index as key. - return
- -
- } else { - return
- - - {mobile && i == 0 && props.data?.introduction && -
- {props.data?.introduction} -
- } - {mobile && <> - - {i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) && - +
+ + {proof.length ? + <> + {proof.map((step, i) => { + if (i == proof.length - 1 && lastStepErrors) { + // if the last command contains an error, we only display the errors but not the + // entered command as it is still present in the command line. + // TODO: Should not use index as key. + return
+ +
+ } else { + return
+ + + {mobile && i == 0 && props.data?.introduction && +
+ {props.data?.introduction} +
} - - } - - {/* Show a message that there are no goals left */} - {!step.goals.length && ( -
- {completed ? -

Level completed! 🎉

: -

- no goals left
- This probably means you solved the level with warnings or Lean encountered a parsing error. -

+ {mobile && <> + + {i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) && + } -
- )} + + } + + {/* Show a message that there are no goals left */} + {!step.goals.length && ( +
+ {completed ? +

Level completed! 🎉

: +

+ no goals left
+ This probably means you solved the level with warnings or Lean encountered a parsing error. +

+ } +
+ )} +
+ } + })} + {mobile && completed && +
+ {props.level >= props.worldSize ? + + : + + }
} - })} - {mobile && completed && -
- {props.level >= props.worldSize ? - - : - - } -
- } -
: <> - } + : <> + } +