diff --git a/client/src/app.tsx b/client/src/app.tsx index b0ef13c..c45f6d0 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -6,33 +6,23 @@ import '@fontsource/roboto/400.css'; import '@fontsource/roboto/500.css'; import '@fontsource/roboto/700.css'; -import './reset.css'; -import './app.css'; +import './css/reset.css'; +import './css/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); function App() { const params = useParams() const gameId = "g/" + params.owner + "/" + params.repo - - // TODO: Make mobileLayout be changeable in settings - // TODO: Handle resize Events 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 index 530636e..2c65a81 100644 --- a/client/src/components/app_bar.tsx +++ b/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) && - } - {(nextText || nextTitle || nextIcon) && + {(nextText || nextIcon) && +} + +/** 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 {mobile, pageNumber, setPageNumber} = React.useContext(MobileContext) - const [navOpen, setNavOpen] = React.useState(false) + const {worldId, levelId} = React.useContext(WorldLevelIdContext) + return (levelId < worldSize ? + + : + + ) +} +/** 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 to toggle between editor and typewriter */ +function InputModeButton({setNavOpen, isDropdown}) { + const {levelId} = React.useContext(WorldLevelIdContext) + const {typewriterMode, setTypewriterMode, lockInputMode} = React.useContext(InputModeContext) - /** 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', - }) + /** toggle input mode if allowed */ + function toggleInputMode(ev: React.MouseEvent) { + if (!lockInputMode){ + setTypewriterMode(!typewriterMode) + setNavOpen(false) + } } + return +} - return
- <> -
- - -
-
- - {mobile ? '' : gameInfo?.title} - -
-
- {mobile && <> - {/* BUTTONS for MOBILE */} - +/** button to toggle iimpressum popup */ +function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) { + return +} - } +/** button to go back to welcome page */ +function HomeButton({isDropdown}) { + const gameId = React.useContext(GameIdContext) + return +} - +/** button in mobile level to toggle inventory. + * only displays a button if `setPageNumber` is set. + */ +function InventoryButton({pageNumber, setPageNumber}) { + return (setPageNumber && + + ) +} -
-
- {/* {levelId < gameInfo.data?.worldSize[worldId] && - - } - {levelId > 0 && <> - - } - - */} +/** 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
+
+ + +
+
+ {!mobile && {gameInfo?.title}} +
+
+ {mobile && } + +
+
+ + + + + +
- - - } -// /** 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, lockEditorMode=false}) { +/** 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 gameInfo = useGetGameInfoQuery({game: gameId}) - const {mobile} = React.useContext(MobileContext) - - const difficulty = useSelector(selectDifficulty(gameId)) - const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) - - const { typewriterMode, setTypewriterMode } = React.useContext(InputModeContext) - const [navOpen, setNavOpen] = React.useState(false) + const gameInfo = useGetGameInfoQuery({game: gameId}) + const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) + const difficulty = useAppSelector(selectDifficulty(gameId)) - function toggleEditor(ev) { - if (!lockEditorMode){ - setTypewriterMode(!typewriterMode) - setNavOpen(false) - } - } + let worldTitle = gameInfo.data?.worlds.nodes[worldId].title return
{mobile ? <> {/* MOBILE VERSION */}
- - {levelTitle} - + {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}`} - + + {worldTitle && `World: ${worldTitle}`}
- - {levelTitle} - + {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 e5b4037..fb0ef2b 100644 --- a/client/src/components/infoview/context.ts +++ b/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>, - pageNumber: number, - setPageNumber: React.Dispatch> }>({ 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>, typewriterInput: string, - setTypewriterInput: React.Dispatch> + setTypewriterInput: React.Dispatch>, + lockInputMode: boolean, + setLockInputMode: React.Dispatch>, }>({ typewriterMode: true, setTypewriterMode: () => {}, typewriterInput: "", setTypewriterInput: () => {}, + lockInputMode: false, + setLockInputMode: () => {}, }); diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 9b84ccf..ab670a1 100644 --- a/client/src/components/infoview/main.tsx +++ b/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'; diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index 5b56503..896b1f7 100644 --- a/client/src/components/inventory.tsx +++ b/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'; diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index 56efea3..f4596b1 100644 --- a/client/src/components/landing_page.tsx +++ b/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' diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index bcbafd9..9e96941 100644 --- a/client/src/components/level.tsx +++ b/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}) {
- + + toggleImpressum={toggleImpressum} /> {mobile? // TODO: This is copied from the `Split` component below... <> @@ -471,7 +471,7 @@ function Introduction({impressum, setImpressum}) { } return <> - + {gameInfo.isLoading ?
: mobile ? diff --git a/client/src/components/popup/erase.tsx b/client/src/components/popup/erase.tsx index 73088f8..b445532 100644 --- a/client/src/components/popup/erase.tsx +++ b/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() } diff --git a/client/src/components/welcome.tsx b/client/src/components/welcome.tsx index c6e2b53..6c6c977 100644 --- a/client/src/components/welcome.tsx +++ b/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}) { : <> ))}
- {/* -

{title}

- {introduction} - - */} {mobile &&