diff --git a/client/src/app.tsx b/client/src/app.tsx index 5b2aadd..bbad3fe 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -9,7 +9,7 @@ import '@fontsource/roboto/700.css'; import './css/reset.css'; import './css/app.css'; -import { PageContext, PreferencesContext} from './components/infoview/context'; +import { GameIdContext, PageContext, PreferencesContext} from './state/context'; import UsePreferences from "./state/hooks/use_preferences" import { Navigation } from './components/navigation'; import { useSelector } from 'react-redux'; @@ -20,11 +20,6 @@ import { useGetGameInfoQuery } from './state/api'; import lean4gameConfig from './config.json' import { useTranslation } from 'react-i18next'; -export const GameIdContext = React.createContext<{ - gameId: string, - worldId: string|null, - levelId: number|null}>({gameId: null, worldId: null, levelId: null}); - function App() { let { t, i18n } = useTranslation() diff --git a/client/src/components/chat.tsx b/client/src/components/chat.tsx index da879de..e915d79 100644 --- a/client/src/components/chat.tsx +++ b/client/src/components/chat.tsx @@ -1,21 +1,23 @@ import * as React from 'react' -import { ChatContext, PageContext, PreferencesContext, ProofContext } from './infoview/context' -import { GameIdContext } from '../app' +import { useContext, useEffect, useRef, useState } from 'react' +import { useSelector } from 'react-redux' import { useTranslation } from 'react-i18next' -import { useAppDispatch, useAppSelector } from '../hooks' -import { Button } from './button' -import { changedReadIntro, selectCompleted, selectReadIntro } from '../state/progress' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faArrowRight } from '@fortawesome/free-solid-svg-icons' + + +import Markdown from './markdown' +import { Button } from './button' + +import { changedReadIntro, selectCompleted, selectReadIntro } from '../state/progress' import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api' -import { useContext, useEffect, useRef, useState } from 'react' +import { useAppDispatch, useAppSelector } from '../hooks' + +import { ChatContext, GameIdContext, PageContext, PreferencesContext, ProofContext } from '../state/context' import { GameHint, InteractiveGoalsWithHints } from './infoview/rpc_api' -import Markdown from './markdown' -import { useSelector } from 'react-redux' import { lastStepHasErrors } from './infoview/goals' import '../css/chat.css' -import { hasErrors } from './infoview/typewriter' /** Split a string by double newlines and filters out empty segments. */ function splitIntro (intro : string) { diff --git a/client/src/components/game.tsx b/client/src/components/game.tsx index 0ea5283..b20cba6 100644 --- a/client/src/components/game.tsx +++ b/client/src/components/game.tsx @@ -1,40 +1,29 @@ import * as React from 'react' import { useContext, useEffect, useRef, useState } from 'react' import Split from 'react-split' -import { Box, CircularProgress } from '@mui/material' -import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { faArrowRight } from '@fortawesome/free-solid-svg-icons' -import { GameIdContext } from '../app' import { useAppDispatch, useAppSelector } from '../hooks' -import { changeTypewriterMode, changedReadIntro, changedSelection, codeEdited, selectCode, selectReadIntro, selectSelections, selectTypewriterMode } from '../state/progress' +import { changeTypewriterMode, selectCode, selectSelections, selectTypewriterMode } from '../state/progress' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api' -import { Button } from './button' -import { ChatContext, PageContext, PreferencesContext, ProofContext } from './infoview/context' +import { ChatContext, GameIdContext, PageContext, PreferencesContext, ProofContext } from '../state/context' import { InventoryPanel } from './inventory' -import { ErasePopup } from './popup/erase' -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' -import '../css/game.css' -import '../css/welcome.css' -import '../css/level.css' import i18next from 'i18next' -import { useTranslation } from 'react-i18next' -import { LoadingIcon } from './utils' import { ChatPanel } from './chat' -import { DualEditor } from './infoview/main' -import { Level, LevelWrapper } from './level' +import { LevelWrapper } from './level' import { GameHint, ProofState } from './infoview/rpc_api' import { useSelector } from 'react-redux' import { Diagnostic } from 'vscode-languageserver-types' +import '../css/game.css' +import '../css/welcome.css' +import '../css/level.css' + /** main page of the game showing among others the tree of worlds/levels */ function Game() { + const dispatch = useAppDispatch() const { gameId, worldId, levelId } = React.useContext(GameIdContext) // Load the namespace of the game @@ -44,16 +33,11 @@ function Game() { const {isSavePreferences, language, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext) const gameInfo = useGetGameInfoQuery({game: gameId}) - const inventory = useLoadInventoryOverviewQuery({game: gameId}) - const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + const inventory = useLoadInventoryOverviewQuery({game: gameId}) const {page, setPage} = useContext(PageContext) - // TODO: recover `readIntro` functionality - - // const [pageNumber, setPageNumber] = React.useState(readIntro ? 1 : 0) - const chatRef = useRef(null) // When deleting the proof, we want to keep to old messages around until // a new proof has been entered. e.g. to consult messages coming from dead ends @@ -71,8 +55,6 @@ function Game() { const [isCrashed, setIsCrashed] = useState(false) - const dispatch = useAppDispatch() - const typewriterMode = useSelector(selectTypewriterMode(gameId)) const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode})) diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx index f340144..d101cbe 100644 --- a/client/src/components/infoview/goals.tsx +++ b/client/src/components/infoview/goals.tsx @@ -9,7 +9,7 @@ import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infov import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation'; import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode' import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips'; -import { PageContext } from './context'; +import { PageContext } from '../../state/context'; import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, InteractiveHypothesisBundle, ProofState } from './rpc_api'; import { RpcSessionAtPos } from '@leanprover/infoview/*'; import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx index 3ade899..ead03f5 100644 --- a/client/src/components/infoview/info.tsx +++ b/client/src/components/infoview/info.tsx @@ -15,7 +15,7 @@ import { GoalsLocation, Locations, LocationsContext } from '../../../../node_mod import { AllMessages, lspDiagToInteractive } from './messages' import { goalsToString, Goal, MainAssumptions, OtherGoals } from './goals' import { InteractiveTermGoal, InteractiveGoalsWithHints, InteractiveGoals, ProofState } from './rpc_api' -import { MonacoEditorContext, ProofStateProps, InfoStatus, ProofContext } from './context' +import { MonacoEditorContext, ProofStateProps, InfoStatus, ProofContext } from '../../state/context' import { useTranslation } from 'react-i18next' // TODO: All about pinning could probably be removed diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 2a4c013..298bb38 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -18,7 +18,6 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faDeleteLeft, faHome, faArrowRight, faArrowLeft, faRotateLeft } from '@fortawesome/free-solid-svg-icons' import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import { GameIdContext } from '../../app'; import { useAppDispatch, useAppSelector } from '../../hooks'; import { LevelInfo, useGetGameInfoQuery, useLoadLevelQuery } from '../../state/api'; import { changedInventory, levelCompleted, selectCode, selectCompleted, selectInventory } from '../../state/progress'; @@ -27,7 +26,7 @@ import Markdown from '../markdown'; import { Infos } from './infos'; import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages'; import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals'; -import { ChatContext, PageContext, PreferencesContext, MonacoEditorContext, ProofContext } from './context'; +import { ChatContext, PageContext, PreferencesContext, MonacoEditorContext, ProofContext, GameIdContext } from '../../state/context'; import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter'; import { InteractiveDiagnostic } from '@leanprover/infoview/*'; import { Button } from '../button'; diff --git a/client/src/components/infoview/messages.tsx b/client/src/components/infoview/messages.tsx index 4dc0123..c1c8f13 100644 --- a/client/src/components/infoview/messages.tsx +++ b/client/src/components/infoview/messages.tsx @@ -10,7 +10,7 @@ import { Details } from '../../../../node_modules/lean4-infoview/src/infoview/co import { InteractiveMessage } from '../../../../node_modules/lean4-infoview/src/infoview/traceExplorer' import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions' -import { PageContext } from './context' +import { PageContext } from '../../state/context' import { useTranslation } from 'react-i18next' interface MessageViewProps { diff --git a/client/src/components/infoview/typewriter.tsx b/client/src/components/infoview/typewriter.tsx index 7269fd0..f9823eb 100644 --- a/client/src/components/infoview/typewriter.tsx +++ b/client/src/components/infoview/typewriter.tsx @@ -17,11 +17,10 @@ import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } fro import { Diagnostic } from 'vscode-languageserver-types'; import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; -import { ChatContext, PageContext, MonacoEditorContext, ProofContext } from './context' +import { ChatContext, PageContext, MonacoEditorContext, ProofContext, GameIdContext } from '../../state/context' import { goalsToString, lastStepHasErrors, loadGoals } from './goals' import { GameHint, ProofState } from './rpc_api' import { useTranslation } from 'react-i18next' -import { GameIdContext } from '../../app' export interface GameDiagnosticsParams { uri: DocumentUri; diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index c047bac..d6150b0 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -4,7 +4,6 @@ import '../css/inventory.css' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faLock, faBan, faCheck, faXmark } from '@fortawesome/free-solid-svg-icons' import { faClipboard } from '@fortawesome/free-regular-svg-icons' -import { GameIdContext } from '../app'; import Markdown from './markdown'; import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api'; import { selectDifficulty, selectInventory } from '../state/progress'; @@ -14,6 +13,7 @@ import { useTranslation } from 'react-i18next'; import { t } from 'i18next'; import { NavButton } from './navigation'; import { LoadingIcon } from './utils'; +import { GameIdContext } from '../state/context'; /** Context which manages the inventory */ diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 6bdc1a4..dbd5695 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -19,7 +19,6 @@ import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/ import { Diagnostic } from 'vscode-languageserver-types' import { DiagnosticSeverity } from 'vscode-languageclient'; -import { GameIdContext } from '../app' import { useAppDispatch, useAppSelector } from '../hooks' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api' import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited, @@ -31,7 +30,7 @@ import {InventoryPanel} from './inventory' import { Editor } from './editor' import { Typewriter } from './typewriter' import { ChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, - ProofContext, PageContext } from './infoview/context' + ProofContext, PageContext, GameIdContext } from '../state/context' import { DualEditor, ExerciseStatement } from './infoview/main' import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api' import path from 'path'; diff --git a/client/src/components/navigation.tsx b/client/src/components/navigation.tsx index 39e68ca..e6bd4ea 100644 --- a/client/src/components/navigation.tsx +++ b/client/src/components/navigation.tsx @@ -4,8 +4,7 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome, faArrowRight, faArrowLeft, faXmark, faBars, faCode, faCircleInfo, faTerminal, faGear, IconDefinition, faShield } from '@fortawesome/free-solid-svg-icons' -import { GameIdContext } from "../app" -import { PageContext, PreferencesContext } from "./infoview/context" +import { GameIdContext, PageContext, PreferencesContext } from "../state/context" import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api' import { downloadProgress } from './popup/erase' import { useTranslation } from 'react-i18next' diff --git a/client/src/components/popup/erase.tsx b/client/src/components/popup/erase.tsx index 8ff0db9..3fc67e1 100644 --- a/client/src/components/popup/erase.tsx +++ b/client/src/components/popup/erase.tsx @@ -1,14 +1,13 @@ 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, Button2 } from '../button' +import { Button } from '../button' import { Trans, useTranslation } from 'react-i18next' import { useContext } from 'react' import { PopupContext } from './popup' -import { PageContext } from '../infoview/context' +import { GameIdContext, PageContext } from '../../state/context' /** download the current progress (i.e. what's saved in the browser store) */ export function downloadProgress(gameId: string, gameProgress) { diff --git a/client/src/components/popup/info.tsx b/client/src/components/popup/info.tsx index 9c4cefb..7ff4f90 100644 --- a/client/src/components/popup/info.tsx +++ b/client/src/components/popup/info.tsx @@ -2,8 +2,8 @@ import * as React from 'react' import { Typography } from '@mui/material' import Markdown from '../markdown' import { Trans, useTranslation } from 'react-i18next' -import { GameIdContext } from '../../app' import { useGetGameInfoQuery } from '../../state/api' +import { GameIdContext } from '../../state/context' /** Pop-up that is displaying the Game Info. * diff --git a/client/src/components/popup/preferences.tsx b/client/src/components/popup/preferences.tsx index 997f827..ac6d8ed 100644 --- a/client/src/components/popup/preferences.tsx +++ b/client/src/components/popup/preferences.tsx @@ -8,7 +8,7 @@ import lean4gameConfig from '../../config.json' import FormControlLabel from '@mui/material/FormControlLabel'; -import { IPreferencesContext, PreferencesContext } from "../infoview/context" +import { IPreferencesContext, PreferencesContext } from "../../state/context" import ReactCountryFlag from 'react-country-flag'; import { useTranslation } from 'react-i18next'; diff --git a/client/src/components/popup/rules.tsx b/client/src/components/popup/rules.tsx index 30f9677..be88c3b 100644 --- a/client/src/components/popup/rules.tsx +++ b/client/src/components/popup/rules.tsx @@ -1,11 +1,11 @@ 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' +import { GameIdContext } from '../../state/context' /** Pop-up that is displayed when opening the help explaining the game rules. * diff --git a/client/src/components/popup/upload.tsx b/client/src/components/popup/upload.tsx index 7519926..5269e29 100644 --- a/client/src/components/popup/upload.tsx +++ b/client/src/components/popup/upload.tsx @@ -3,7 +3,6 @@ */ 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' @@ -11,6 +10,7 @@ import { Button } from '../button' import { Trans, useTranslation } from 'react-i18next' import { PopupContext } from './popup' import { useContext } from 'react' +import { GameIdContext } from '../../state/context' /** Pop-up that is displaying the Game Info. * diff --git a/client/src/components/welcome.tsx b/client/src/components/welcome.tsx deleted file mode 100644 index fb6a80e..0000000 --- a/client/src/components/welcome.tsx +++ /dev/null @@ -1,151 +0,0 @@ -import * as React from 'react' -import { useEffect } from 'react' -import Split from 'react-split' -import { Box, CircularProgress } from '@mui/material' -import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { faArrowRight } from '@fortawesome/free-solid-svg-icons' - -import { GameIdContext } from '../app' -import { useAppDispatch, useAppSelector } from '../hooks' -import { changedReadIntro, selectReadIntro } from '../state/progress' -import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api' -import { Button } from './button' -import { PageContext, PreferencesContext } from './infoview/context' -import { InventoryPanel } from './inventory' -import { ErasePopup } from './popup/erase' -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' - -import '../css/welcome.css' -import { Hint } from './hints' -import i18next from 'i18next' -import { useTranslation } from 'react-i18next' - - -/** the panel showing the game's introduction text */ -function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) { - const {mobile} = React.useContext(PreferencesContext) - const {gameId} = React.useContext(GameIdContext) - - let { t } = useTranslation() - - const dispatch = useAppDispatch() - - // TODO: I left the setup for splitting up the introduction in place, but if it's not needed - // then this can be simplified. - - // let text: Array = introduction.split(/\n(\s*\n)+/) - let text: Array = introduction ? [t(introduction, {ns : gameId})] : [] - - return
-
- {text?.map(((t, i) => - t.trim() ? - - : <> - ))} -
- {mobile && -
- -
- } -
-} - -/** main page of the game showing among others the tree of worlds/levels */ -function Welcome() { - const {gameId, worldId} = React.useContext(GameIdContext) - - // Load the namespace of the game - i18next.loadNamespaces(gameId) - - const {mobile} = React.useContext(PreferencesContext) - const {layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext) - - const gameInfo = useGetGameInfoQuery({game: gameId}) - const inventory = useLoadInventoryOverviewQuery({game: gameId}) - - // For mobile only - const readIntro = useAppSelector(selectReadIntro(gameId, worldId)) - - const {page, setPage} = React.useContext(PageContext) - - // TODO: recover `readIntro` functionality - - // const [pageNumber, setPageNumber] = React.useState(readIntro ? 1 : 0) - - // pop-ups - const [eraseMenu, setEraseMenu] = React.useState(false) - const [impressum, setImpressum] = React.useState(false) - const [privacy, setPrivacy] = React.useState(false) - const [info, setInfo] = React.useState(false) - const [rulesHelp, setRulesHelp] = React.useState(false) - const [uploadMenu, setUploadMenu] = React.useState(false) - const [preferencesPopup, setPreferencesPopup] = React.useState(false) - - function closeEraseMenu() {setEraseMenu(false)} - function closeImpressum() {setImpressum(false)} - function closePrivacy() {setPrivacy(false)} - function closeInfo() {setInfo(false)} - function closeRulesHelp() {setRulesHelp(false)} - function closeUploadMenu() {setUploadMenu(false)} - function closePreferencesPopup() {setPreferencesPopup(false)} - function toggleEraseMenu() {setEraseMenu(!eraseMenu)} - function toggleImpressum() {setImpressum(!impressum)} - function togglePrivacy() {setPrivacy(!privacy)} - function toggleInfo() {setInfo(!info)} - function toggleUploadMenu() {setUploadMenu(!uploadMenu)} - function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)} - - // set the window title - useEffect(() => { - if (gameInfo.data?.title) { - window.document.title = gameInfo.data.title - } - }, [gameInfo.data?.title]) - - return gameInfo.isLoading ? - - - - : <> - {/* */} -
- { mobile ? -
- {(page == 0 ? - - : page == 1 ? - - : - - )} -
- : - - - - - - } -
- -} - -export default Welcome diff --git a/client/src/components/world_tree.tsx b/client/src/components/world_tree.tsx index f4d6361..165cc95 100644 --- a/client/src/components/world_tree.tsx +++ b/client/src/components/world_tree.tsx @@ -10,13 +10,12 @@ import klay from 'cytoscape-klay' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons' -import { GameIdContext } from '../app' import { useAppDispatch } from '../hooks' import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress' import { store } from '../state/store' import '../css/world_tree.css' -import { PreferencesContext } from './infoview/context' +import { GameIdContext, PreferencesContext } from '../state/context' import { useTranslation } from 'react-i18next' import { useGetGameInfoQuery } from '../state/api' import { LoadingIcon } from './utils' diff --git a/client/src/components/infoview/context.ts b/client/src/state/context.ts similarity index 94% rename from client/src/components/infoview/context.ts rename to client/src/state/context.ts index 3f13dcb..b9d10c0 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/state/context.ts @@ -5,14 +5,20 @@ import * as React from 'react'; import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import { InteractiveDiagnostic } from '@leanprover/infoview-api'; import { Diagnostic } from 'vscode-languageserver-types' -import { GameHint, InteractiveGoal, InteractiveTermGoal,InteractiveGoalsWithHints, ProofState } from './rpc_api'; -import { PreferencesState } from '../../state/preferences'; +import { GameHint, InteractiveGoal, InteractiveTermGoal,InteractiveGoalsWithHints, ProofState } from '../components/infoview/rpc_api'; +import { PreferencesState } from './preferences'; export const MonacoEditorContext = React.createContext( null as any) export type InfoStatus = 'updating' | 'error' | 'ready'; + +export const GameIdContext = React.createContext<{ + gameId: string, + worldId: string|null, + levelId: number|null}>({gameId: null, worldId: null, levelId: null}); + // /** One step of the proof */ // export type ProofStep = { // /** The command in this step */