From adeed03da81fa554115cd31347798e8d78714435 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 5 Jun 2024 18:41:01 +0200 Subject: [PATCH] cleanup; including cleaning up chat --- client/src/app.tsx | 10 +- client/src/components/chat.tsx | 302 ++++++++- client/src/components/editor.tsx | 7 + client/src/components/game.tsx | 103 +-- client/src/components/hints.tsx | 125 ---- client/src/components/infoview/context.ts | 19 +- client/src/components/infoview/main.tsx | 62 +- client/src/components/infoview/rpc_api.ts | 2 +- client/src/components/infoview/typewriter.tsx | 24 +- client/src/components/inventory.tsx | 29 +- client/src/components/landing_page.tsx | 2 +- client/src/components/level.tsx | 597 ++++++++++-------- client/src/components/navigation.tsx | 39 +- client/src/components/popup/popup.tsx | 4 +- client/src/components/typewriter.tsx | 7 + client/src/components/welcome.tsx | 12 +- client/src/components/world_tree.tsx | 43 +- client/src/config.json | 2 +- client/src/css/chat.css | 21 +- client/src/css/game.css | 5 + client/src/css/infoview.css | 17 - client/src/css/inventory.css | 5 + client/src/css/level.css | 65 +- client/src/css/navigation.css | 20 + client/src/index.tsx | 1 - client/src/state/api.ts | 2 +- client/src/state/progress.ts | 64 +- 27 files changed, 934 insertions(+), 655 deletions(-) create mode 100644 client/src/components/editor.tsx delete mode 100644 client/src/components/hints.tsx create mode 100644 client/src/components/typewriter.tsx diff --git a/client/src/app.tsx b/client/src/app.tsx index 9c15c84..5b2aadd 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -1,6 +1,6 @@ import * as React from 'react'; import { Outlet, useParams, useSearchParams } from "react-router-dom"; -import { useEffect, useState } from 'react'; +import { Suspense, useEffect, useState } from 'react'; import '@fontsource/roboto/300.css'; import '@fontsource/roboto/400.css'; @@ -13,7 +13,7 @@ import { PageContext, PreferencesContext} from './components/infoview/context'; import UsePreferences from "./state/hooks/use_preferences" import { Navigation } from './components/navigation'; import { useSelector } from 'react-redux'; -import { changeTypewriterMode, selectOpenedIntro, selectTypewriterMode } from './state/progress'; +import { changeTypewriterMode, selectReadIntro, selectTypewriterMode } from './state/progress'; import { useAppDispatch } from './hooks'; import { Popup, PopupContext } from './components/popup/popup'; import { useGetGameInfoQuery } from './state/api'; @@ -45,7 +45,7 @@ function App() { const gameInfo = useGetGameInfoQuery({game: gameId}) const [searchParams, setSearchParams] = useSearchParams() - const openedIntro = useSelector(selectOpenedIntro(gameId)) + const readIntro = useSelector(selectReadIntro(gameId, worldId)) // mobile only: game intro should only be shown once and skipped afterwards useEffect(() => { @@ -53,14 +53,14 @@ function App() { console.log('setting page to 1') setPage(1) } else { - if (openedIntro && page == 0) { + if (readIntro && page == 0) { console.log('setting page to 1') setPage(1) } else { // setPage(0) } } - }, [openedIntro, worldId, levelId]) + }, [worldId, levelId]) // option to pass language as `?lang=de` in the URL useEffect(() => { diff --git a/client/src/components/chat.tsx b/client/src/components/chat.tsx index 4ce6602..8b734ff 100644 --- a/client/src/components/chat.tsx +++ b/client/src/components/chat.tsx @@ -1,15 +1,19 @@ import * as React from 'react' -import { PageContext, PreferencesContext } from './infoview/context' +import { ChatContext, PageContext, PreferencesContext, ProofContext } from './infoview/context' import { GameIdContext } from '../app' import { useTranslation } from 'react-i18next' -import { useAppDispatch } from '../hooks' -import { Hint } from './hints' +import { useAppDispatch, useAppSelector } from '../hooks' import { Button } from './button' -import { changedOpenedIntro } from '../state/progress' +import { changedReadIntro, selectCompleted, selectReadIntro } from '../state/progress' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faArrowRight } from '@fortawesome/free-solid-svg-icons' import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api' import { useContext, useEffect, useRef, useState } from 'react' +import { GameHint, InteractiveGoalsWithHints } from './infoview/rpc_api' +import Markdown from './markdown' +import { useSelector } from 'react-redux' +import { lastStepHasErrors } from './infoview/goals' + import '../css/level.css' import '../css/chat.css' @@ -18,33 +22,236 @@ function splitIntro (intro : string) { return intro.split(/\n(\s*\n)+/).filter(t => t.trim()) } -/** The buttons at the bottom of chat */ -export function ChatButtons () { +/** Helper to check if a step has any hidden hints. */ +function hasHiddenHints(step: InteractiveGoalsWithHints): boolean { + return step?.goals[0]?.hints.some((hint) => hint.hidden) +} + +/** Button which only appears if the current step has hidden hints that are not shown yet. */ +export function MoreHelpButton({selected=null} : {selected?: number}) { + + const { t } = useTranslation() + + const { proof } = React.useContext(ProofContext) + const { showHelp, setShowHelp } = React.useContext(ChatContext) + + let k = proof?.steps.length ? + ((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected) + : 0 + + const activateHiddenHints = (ev) => { + // If the last step (`k`) has errors, we want the hidden hints from the + // second-to-last step to be affected + if (!(proof?.steps.length)) {return <>} + + // state must not be mutated, therefore we need to clone the set + let tmp = new Set(showHelp) + if (tmp.has(k)) { + tmp.delete(k) + } else { + tmp.add(k) + } + setShowHelp(tmp) + console.debug(`help: ${Array.from(tmp.values())}`) + } + + if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) { + return + } +} + +/** Placeholder that takes the same space as a button. */ +function ButtonPlaceholder() { + return
+} + +/** The buttons at the bottom of chat. */ +export function ChatButtons ({counter=undefined, setCounter=()=>{}, introMessages=[]} : { + counter?: number + setCounter?: React.Dispatch> + introMessages?: GameHintWithStep[] +}) { + const { mobile } = useContext(PreferencesContext) const { gameId, worldId, levelId } = useContext(GameIdContext) const {setPage} = useContext(PageContext) const dispatch = useAppDispatch() const gameInfo = useGetGameInfoQuery({game: gameId}) + const readIntro = useSelector(selectReadIntro(gameId, worldId)) + return
- {(!worldId || !levelId) && + {/* { ((mobile && !worldId) || worldId && !levelId) && // Start button appears only on world selection and level 0. + } */} + {!levelId && (readIntro || (counter >= introMessages.length) ? + ((worldId || mobile) && + <> + + + + ) + : + <> + + + + + )} + { worldId && levelId && } +
+} + +/** Insert the variable names in a hint. We do this client-side to prepare + * for i18n in the future. i.e. one should be able translate the `rawText` + * and have the variables substituted just before displaying. + */ +function getHintText(hint: GameHint): string { + const {gameId} = React.useContext(GameIdContext) + let { t } = useTranslation() + if (hint.rawText) { + // Replace the variable names used in the hint with the ones used by the player + // variable names are marked like `«{g}»` inside the text. + return t(hint.rawText, {ns: gameId}).replaceAll(/«\{(.*?)\}»/g, ((_, v) => + // `hint.varNames` contains tuples `[oldName, newName]` + (hint.varNames.find(x => x[0] == v))[1])) + } else { + // hints created in the frontend do not have a `rawText` + // TODO: `hint.text` could be removed in theory. + return t(hint.text, {ns: gameId}) + } +} + +/** Bundling a hint with the proof-step it comes from. */ +type GameHintWithStep = { + hint: GameHint + step?: number + conclusion?: boolean +} + +/** Filter hints to not show consequtive identical hints twice. + * Hidden hints are not filtered. + */ +export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] { + if (!hints) { + return [] + } else if (!prevHints) { + return [...hints.filter((hint) => !hint.hidden), ...hints.filter((hint) => hint.hidden)] + } else { + return [...hints.filter((hint) => !hint.hidden && + (prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined) + ), ...hints.filter((hint) => hint.hidden)] + } +} + +/** A hint as it is displayed in the chat. */ +export function Hint({hint, step=null, conclusion=false} : GameHintWithStep) { + const { levelId } = useContext(GameIdContext) + const { selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp } = useContext(ChatContext) + + const { proof } = useContext(ProofContext) + const { typewriterMode } = useContext(PageContext) + + function toggleSelection () { + if (!levelId) {return} + + if (selectedStep !== null && selectedStep == step) { + setSelectedStep(undefined) + } else if (step < proof?.steps?.length) { + setSelectedStep(step) } + } + + // "Deleted hints" are marked in grey. They are used two-fold: + // In typewriter, deleting parts of the proof stores the removed hints as `deletedChat` + // until the next command is submitted; in editor, moving the cursor through the proof will + // render all hints + return
= (typewriterMode ? proof?.steps?.length : selectedStep+1) ? ' deleted-hint' : '') } onClick={toggleSelection}> + {getHintText(hint)}
} +/** A collection of hints. If the `counter` is defined, only the first elements will be + * shown up to the value of the `counter`. + * + * Set `conclusion` to true to trigger different style and disable selecting/deleting. + */ +export function Hints({ hints, conclusion, counter=undefined } : { + hints: GameHintWithStep[], + conclusion?: boolean, + counter?: number +}) { + + const { showHelp } = useContext(ChatContext) + + if (!hints) { + return <> + } + + // NOTE: This builds on the fact that `.slice(0, undefined)` returns the whole array! + // TODO: Should not use index as key. + return <> + { hints.slice(0, counter).map((hint, j) => + ((!hint.hint.hidden || showHelp.has(hint.step)) && + + ) + )} + {/* { //showHelp.has(hint.step) && + hints.filter(hint => hint.hint.hidden).map((hint, j) => + + )} */} + +} + /** the panel showing the game's introduction text */ export function ChatPanel ({visible = true}) { @@ -54,51 +261,100 @@ export function ChatPanel ({visible = true}) { const { mobile } = useContext(PreferencesContext) const { gameId, worldId, levelId } = useContext(GameIdContext) + const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) + const gameInfo = useGetGameInfoQuery({game: gameId}) const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) - let [chatMessages, setChatMessages] = useState>([]) + let [counter, setCounter] = useState(1) + + let [introText, setIntroText] = useState>([]) + let [chatMessages, setChatMessages] = useState>([]) + let { deletedChat } = useContext(ChatContext) + let {proof} = useContext(ProofContext) - // Effect to clear chat and display the correct intro text + const readIntro = useSelector(selectReadIntro(gameId, worldId)) + + useEffect(() => { + setCounter(1) + }, [gameId, worldId, levelId]) + + // load and display the correct intro text useEffect(() => { + let messages: GameHintWithStep[] = [] + if (levelId > 0) { + let introText = t(levelInfo.data?.introduction, {ns : gameId}).trim() + let introHint: GameHintWithStep = {hint: {text: introText, hidden: false, rawText: introText }, step: 0} + // playable level: show the level's intro if (levelInfo.data?.introduction) { - setChatMessages([t(levelInfo.data?.introduction, {ns : gameId})]) + setIntroText([introHint]) + // messages = messages.concat([introHint]) } else { - setChatMessages([]) + setIntroText([]) } + + proof?.steps?.forEach((step, i) => { + console.log("tesr") + messages = messages.concat(filterHints(step.goals[0]?.hints, proof.steps[i-1]?.goals[0]?.hints).map(hint => ({hint: hint, step: i}))) + }) + } else { if (worldId) { + let introText = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).trim() + let introHints: GameHintWithStep[] = splitIntro(introText).map( txt => ({hint: {text: txt, hidden: false, rawText: txt }, step: 0})) + // Level 0: show the world's intro if (gameInfo.data?.worlds.nodes[worldId].introduction) { - setChatMessages(splitIntro(t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}))) + // messages = messages.concat(introHints) + setIntroText(introHints) } else { - setChatMessages([]) + setIntroText([]) } } else { + let introText = t(gameInfo.data?.introduction, {ns : gameId}).trim() + let introHints: GameHintWithStep[] = splitIntro(introText).map( txt => ({hint: {text: txt, hidden: false, rawText: txt }, step: 0})) + // world overview: show the game's intro if (gameInfo.data?.introduction) { - setChatMessages(splitIntro(t(gameInfo.data?.introduction, {ns : gameId}))) + // messages = messages.concat(introHints) + setIntroText(introHints) } else { - setChatMessages([]) + setIntroText([]) } } } - }, [gameInfo, levelInfo, gameId, worldId, levelId]) + console.log('chat messages:') + console.log(messages) + setChatMessages(messages) + }, [gameInfo, levelInfo, gameId, worldId, levelId, proof]) return
-
+
+ + + {/* {proof?.steps.map((step, i) => + ({hint: hint, step: i}))}/> + )} */} + {/* ({hint: hint, step: proof?.steps?.length - 1}))} /> */} + + { deletedChat && + ({hint: hint, step: proof?.steps?.length}))} /> + } + { completed && levelInfo.data?.conclusion && + + } - {chatMessages.map(((t, i) => + {/* {chatMessages.map(((t, i) => t.trim() ? + step={0} /> : <> - ))} + ))} */}
- { mobile && } + { }
} diff --git a/client/src/components/editor.tsx b/client/src/components/editor.tsx new file mode 100644 index 0000000..ee5ace7 --- /dev/null +++ b/client/src/components/editor.tsx @@ -0,0 +1,7 @@ +import * as React from 'react' + +export function Editor () { + return

+ I'm an editor +

+} diff --git a/client/src/components/game.tsx b/client/src/components/game.tsx index 45a2b31..75e6d5a 100644 --- a/client/src/components/game.tsx +++ b/client/src/components/game.tsx @@ -1,5 +1,5 @@ import * as React from 'react' -import { useEffect, useRef } 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' @@ -7,10 +7,10 @@ import { faArrowRight } from '@fortawesome/free-solid-svg-icons' import { GameIdContext } from '../app' import { useAppDispatch, useAppSelector } from '../hooks' -import { changedOpenedIntro, selectOpenedIntro } from '../state/progress' +import { changeTypewriterMode, changedReadIntro, changedSelection, codeEdited, selectCode, selectReadIntro, selectSelections, selectTypewriterMode } from '../state/progress' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api' import { Button } from './button' -import { PageContext, PreferencesContext } from './infoview/context' +import { ChatContext, PageContext, PreferencesContext, ProofContext } from './infoview/context' import { InventoryPanel } from './inventory' import { ErasePopup } from './popup/erase' import { InfoPopup } from './popup/info' @@ -22,25 +22,25 @@ import { WorldTreePanel } from './world_tree' import '../css/game.css' import '../css/welcome.css' import '../css/level.css' -import { Hint } from './hints' import i18next from 'i18next' import { useTranslation } from 'react-i18next' import { LoadingIcon } from './utils' import { ChatPanel } from './chat' import { DualEditor } from './infoview/main' -import { Level } from './level' +import { Level, LevelWrapper } from './level' +import { GameHint, ProofState } from './infoview/rpc_api' +import { useSelector } from 'react-redux' +import { Diagnostic } from 'vscode-languageserver-types' /** main page of the game showing among others the tree of worlds/levels */ function Game() { - const codeviewRef = useRef(null) - const { gameId, worldId, levelId } = React.useContext(GameIdContext) // Load the namespace of the game i18next.loadNamespaces(gameId) - const {mobile} = React.useContext(PreferencesContext) + const {mobile} = useContext(PreferencesContext) const {isSavePreferences, language, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext) const gameInfo = useGetGameInfoQuery({game: gameId}) @@ -48,21 +48,35 @@ function Game() { const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + const {page, setPage} = useContext(PageContext) + + // TODO: recover `readIntro` functionality + + // const [pageNumber, setPageNumber] = React.useState(readIntro ? 1 : 0) + + // 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 + const [deletedChat, setDeletedChat] = useState>([]) + // A set of row numbers where help is displayed + const [showHelp, setShowHelp] = useState>(new Set()) + // Select and highlight proof steps and corresponding hints + // TODO: with the new design, there is no difference between the introduction and + // a hint at the beginning of the proof... + const [selectedStep, setSelectedStep] = useState(null) - const {page, setPage} = React.useContext(PageContext) + // The state variables for the `ProofContext` + const [proof, setProof] = useState({steps: [], diagnostics: [], completed: false, completedWithWarnings: false}) + const [interimDiags, setInterimDiags] = useState>([]) + const [isCrashed, setIsCrashed] = useState(false) - // TODO: recover `openedIntro` functionality - // const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0) + const dispatch = useAppDispatch() - // 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) + const typewriterMode = useSelector(selectTypewriterMode(gameId)) + const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode})) + + const initialCode = useAppSelector(selectCode(gameId, worldId, levelId)) + const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId)) // set the window title useEffect(() => { @@ -71,27 +85,40 @@ function Game() { } }, [gameInfo.data?.title]) - return mobile ? -
- {<> - - { worldId ? - 0 && page == 1} /> : - + // Delete the current proof on changing level + useEffect(() => { + setProof(null) + setSelectedStep(null) + setDeletedChat([]) + setShowHelp(new Set()) + }, [gameId, worldId, levelId]) + + return + + { mobile ? +
+ {<> + + { worldId ? + (levelId > 0 && ) : + + } + + } - - - } -
- : - - -
- {/* Note: apparently without this `div` the split panel bugs out. */} - {worldId ? : }
- - + : + + +
+ {/* Note: apparently without this `div` the split panel bugs out. */} + {worldId ? (levelId > 0 && ) : } +
+ + + } + + } diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx deleted file mode 100644 index 257e521..0000000 --- a/client/src/components/hints.tsx +++ /dev/null @@ -1,125 +0,0 @@ -import { GameHint, InteractiveGoalsWithHints, ProofState } from "./infoview/rpc_api"; -import * as React from 'react'; -import Markdown from './markdown'; -import { DeletedChatContext, ProofContext } from "./infoview/context"; -import { lastStepHasErrors } from "./infoview/goals"; -import { Button } from "./button"; -import { useTranslation } from "react-i18next"; -import { GameIdContext } from "../app"; - -/** Plug-in the variable names in a hint. We do this client-side to prepare - * for i18n in the future. i.e. one should be able translate the `rawText` - * and have the variables substituted just before displaying. - */ -function getHintText(hint: GameHint): string { - const {gameId} = React.useContext(GameIdContext) - let { t } = useTranslation() - if (hint.rawText) { - // Replace the variable names used in the hint with the ones used by the player - // variable names are marked like `«{g}»` inside the text. - return t(hint.rawText, {ns: gameId}).replaceAll(/«\{(.*?)\}»/g, ((_, v) => - // `hint.varNames` contains tuples `[oldName, newName]` - (hint.varNames.find(x => x[0] == v))[1])) - } else { - // hints created in the frontend do not have a `rawText` - // TODO: `hint.text` could be removed in theory. - return t(hint.text, {ns: gameId}) - } -} - -export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) { - return
- {getHintText(hint)} -
-} - -export function HiddenHint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) { - return
- {getHintText(hint)} -
-} - -export function Hints({hints, showHidden, step, selected, toggleSelection, lastLevel} : {hints: GameHint[], showHidden: boolean, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) { - if (!hints) {return <>} - const openHints = hints.filter(hint => !hint.hidden) - const hiddenHints = hints.filter(hint => hint.hidden) - - // TODO: Should not use index as key. - return <> - {openHints.map((hint, j) => )} - {showHidden && hiddenHints.map((hint, j) => )} - -} - -export function DeletedHint({hint} : {hint: GameHint}) { - return
- {getHintText(hint)} -
-} - -export function DeletedHints({hints} : {hints: GameHint[]}) { - - const openHints = hints.filter(hint => !hint.hidden) - const hiddenHints = hints.filter(hint => hint.hidden) - - // TODO: Should not use index as key. - return <> - {openHints.map((hint, i) => )} - {hiddenHints.map((hint, i) => )} - -} - -/** Filter hints to not show consequtive identical hints twice. - * Hidden hints are not filtered. - */ -export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] { - if (!hints) { - return []} - else if (!prevHints) { - return hints } - else { - return hints.filter((hint) => hint.hidden || - (prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined) - ) - } -} - - -function hasHiddenHints(step: InteractiveGoalsWithHints): boolean { - return step?.goals[0]?.hints.some((hint) => hint.hidden) -} - - -export function MoreHelpButton({selected=null} : {selected?: number}) { - - const { t } = useTranslation() - - const {proof, setProof} = React.useContext(ProofContext) - const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext) - - let k = proof?.steps.length ? - ((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected) - : 0 - - const activateHiddenHints = (ev) => { - // If the last step (`k`) has errors, we want the hidden hints from the - // second-to-last step to be affected - if (!(proof?.steps.length)) {return} - - // state must not be mutated, therefore we need to clone the set - let tmp = new Set(showHelp) - if (tmp.has(k)) { - tmp.delete(k) - } else { - tmp.add(k) - } - setShowHelp(tmp) - console.debug(`help: ${Array.from(tmp.values())}`) - } - - if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) { - return - } -} diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts index 363d5c9..afa5d5d 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/components/infoview/context.ts @@ -93,30 +93,17 @@ export const PreferencesContext = React.createContext({ setLanguage: () => {}, }) -export const WorldLevelIdContext = React.createContext<{ - worldId : string, - levelId: number -}>({ - worldId : null, - levelId: 0, -}) -/** Context to keep highlight selected proof step and corresponding chat messages. */ -export const SelectionContext = React.createContext<{ +export const ChatContext = React.createContext<{ selectedStep : number, setSelectedStep: React.Dispatch> -}>({ - selectedStep : undefined, - setSelectedStep: () => {} -}) - -/** Context for deleted Hints that are visible just a bit after they've been deleted */ -export const DeletedChatContext = React.createContext<{ deletedChat : GameHint[], setDeletedChat: React.Dispatch>> showHelp : Set, setShowHelp: React.Dispatch>> }>({ + selectedStep : undefined, + setSelectedStep: () => {}, deletedChat: undefined, setDeletedChat: () => {}, showHelp: undefined, diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 5d1bc79..a4cb524 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -20,25 +20,26 @@ import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import { GameIdContext } from '../../app'; import { useAppDispatch, useAppSelector } from '../../hooks'; -import { LevelInfo, useGetGameInfoQuery } from '../../state/api'; +import { LevelInfo, useGetGameInfoQuery, useLoadLevelQuery } from '../../state/api'; import { changedInventory, levelCompleted, selectCode, selectCompleted, selectInventory } from '../../state/progress'; import Markdown from '../markdown'; import { Infos } from './infos'; import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages'; import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals'; -import { DeletedChatContext, PageContext, PreferencesContext, MonacoEditorContext, ProofContext, SelectionContext, WorldLevelIdContext } from './context'; +import { ChatContext, PageContext, PreferencesContext, MonacoEditorContext, ProofContext } from './context'; import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter'; import { InteractiveDiagnostic } from '@leanprover/infoview/*'; import { Button } from '../button'; import { CircularProgress } from '@mui/material'; import { GameHint, InteractiveGoalsWithHints, ProofState } from './rpc_api'; import { store } from '../../state/store'; -import { Hints, MoreHelpButton, filterHints } from '../hints'; import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; import { DiagnosticSeverity } from 'vscode-languageclient'; import { useTranslation } from 'react-i18next'; import path from 'path'; +import { useContext } from 'react'; +import { Hints, MoreHelpButton, filterHints } from '../chat'; /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is @@ -49,7 +50,7 @@ export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize }) const { typewriterMode, lockEditorMode } = React.useContext(PageContext) return <>
- + {/* */}
{ec ? @@ -135,23 +136,24 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin * * If `showLeanStatement` is true, it will additionally display the lean code. */ -function ExerciseStatement({ data, showLeanStatement = false }) { +export function ExerciseStatement({ showLeanStatement = false }) { let { t } = useTranslation() - const {gameId} = React.useContext(GameIdContext) + const {gameId, worldId, levelId } = React.useContext(GameIdContext) + const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) - if (!(data?.descrText || data?.descrFormat)) { return <> } + if (!(levelInfo.data?.descrText || levelInfo.data?.descrFormat)) { return <> } return <>
- {data?.descrText ? + {levelInfo.data?.descrText ? - {(data?.displayName ? `**${t("Theorem")}** \`${data?.displayName}\`: ` : '') + t(data?.descrText, {ns: gameId})} - : data?.displayName && + {(levelInfo.data?.displayName ? `**${t("Theorem")}** \`${levelInfo.data?.displayName}\`: ` : '') + t(levelInfo.data?.descrText, {ns: gameId})} + : levelInfo.data?.displayName && - {`**${t("Theorem")}** \`${data?.displayName}\``} + {`**${t("Theorem")}** \`${levelInfo.data?.displayName}\``} } - {data?.descrFormat && showLeanStatement && -

{data?.descrFormat}

+ {levelInfo.data?.descrFormat && showLeanStatement && +

{levelInfo.data?.descrFormat}

}
@@ -162,13 +164,10 @@ function ExerciseStatement({ data, showLeanStatement = false }) { export function Main(props: { world: string, level: number, data: LevelInfo}) { let { t } = useTranslation() const ec = React.useContext(EditorContext); - const {gameId} = React.useContext(GameIdContext) - const {worldId, levelId} = React.useContext(WorldLevelIdContext) + const {gameId, worldId, levelId} = React.useContext(GameIdContext) const { proof, setProof } = React.useContext(ProofContext) - const {selectedStep, setSelectedStep} = React.useContext(SelectionContext) - const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext) - + const {selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp} = React.useContext(ChatContext) function toggleSelection(line: number) { return (ev) => { @@ -249,11 +248,11 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
} - - + */}
} @@ -403,23 +402,21 @@ export function TypewriterInterfaceWrapper(props: { world: string, level: number export function TypewriterInterface({props}) { let { t } = useTranslation() const ec = React.useContext(EditorContext) - const {gameId} = React.useContext(GameIdContext) + const {gameId,worldId, levelId} = React.useContext(GameIdContext) const editor = React.useContext(MonacoEditorContext) const model = editor.getModel() const uri = model.uri.toString() const gameInfo = useGetGameInfoQuery({game: gameId}) - const {worldId, levelId} = React.useContext(WorldLevelIdContext) let image: string = gameInfo.data?.worlds.nodes[worldId].image const [disableInput, setDisableInput] = React.useState(false) const [loadingProgress, setLoadingProgress] = React.useState(0) - const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext) + const { selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp } = React.useContext(ChatContext) const {mobile} = React.useContext(PreferencesContext) const { proof, setProof, crashed, setCrashed, interimDiags } = React.useContext(ProofContext) const { setTypewriterInput } = React.useContext(PageContext) - const { selectedStep, setSelectedStep } = React.useContext(SelectionContext) const proofPanelRef = React.useRef(null) // const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig; @@ -513,19 +510,19 @@ export function TypewriterInterface({props}) { return
-
+ {/*
{image && } -
-
- {/*
+
*/} + {/*
+
-
*/} -
+
+
*/}
- + {/* */} {crashed ?

{t("Crashed! Go to editor mode and fix your proof! Last server response:")}

{interimDiags.map(diag => { @@ -569,8 +566,7 @@ export function TypewriterInterface({props}) { } {mobile && + hints={filteredHints.map(hint => ({hint: hint, step: i}))} /> } {/* setDisableInput(n > 0) : (n) => {}}/> */} {!(isLastStepWithErrors(proof, i)) && diff --git a/client/src/components/infoview/rpc_api.ts b/client/src/components/infoview/rpc_api.ts index 3a6acba..bf15a1b 100644 --- a/client/src/components/infoview/rpc_api.ts +++ b/client/src/components/infoview/rpc_api.ts @@ -50,7 +50,7 @@ export interface GameHint { text: string; hidden: boolean; rawText: string; - varNames: string[][]; // in Lean: `Array (Name × Name)` + varNames?: string[][]; // in Lean: `Array (Name × Name)` } export interface InteractiveGoalWithHints { diff --git a/client/src/components/infoview/typewriter.tsx b/client/src/components/infoview/typewriter.tsx index 3488aa6..7269fd0 100644 --- a/client/src/components/infoview/typewriter.tsx +++ b/client/src/components/infoview/typewriter.tsx @@ -17,10 +17,11 @@ 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 { DeletedChatContext, PageContext, MonacoEditorContext, ProofContext } from './context' +import { ChatContext, PageContext, MonacoEditorContext, ProofContext } from './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; @@ -81,8 +82,8 @@ export function Typewriter({disabled}: {disabled?: boolean}) { /** Reference to the hidden multi-line editor */ const editor = React.useContext(MonacoEditorContext) - const model = editor.getModel() - const uri = model.uri.toString() + const model = editor?.getModel() + const uri = model?.uri.toString() const [oneLineEditor, setOneLineEditor] = useState(null) const [processing, setProcessing] = useState(false) @@ -94,8 +95,10 @@ export function Typewriter({disabled}: {disabled?: boolean}) { // The context storing all information about the current proof const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext) + const {gameId, worldId, levelId} = React.useContext(GameIdContext) + // state to store the last batch of deleted messages - const {setDeletedChat} = React.useContext(DeletedChatContext) + const {setDeletedChat} = React.useContext(ChatContext) const rpcSess = React.useContext(RpcContext) @@ -106,13 +109,13 @@ export function Typewriter({disabled}: {disabled?: boolean}) { // TODO: Desired logic is to only reset this after a new *error-free* command has been entered setDeletedChat([]) - const pos = editor.getPosition() + const pos = editor?.getPosition() if (typewriterInput) { setProcessing(true) - editor.executeEdits("typewriter", [{ + editor?.executeEdits("typewriter", [{ range: monaco.Selection.fromPositions( pos, - editor.getModel().getFullModelRange().getEndPosition() + editor?.getModel()?.getFullModelRange()?.getEndPosition() ), text: typewriterInput.trim() + "\n", forceMoveMarkers: false @@ -122,7 +125,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) { loadGoals(rpcSess, uri, setProof, setCrashed) } - editor.setPosition(pos) + editor?.setPosition(pos) }, [typewriterInput, editor]) useEffect(() => { @@ -133,8 +136,9 @@ export function Typewriter({disabled}: {disabled?: boolean}) { /* Load proof on start/switching to typewriter */ useEffect(() => { + setProof(null) loadGoals(rpcSess, uri, setProof, setCrashed) - }, []) + }, [gameId, worldId, levelId]) /** If the last step has an error, add the command to the typewriter. */ useEffect(() => { @@ -157,7 +161,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) { // TODO: loadAllGoals() if (!hasErrors(params.diagnostics)) { //setTypewriterInput("") - editor.setPosition(editor.getModel().getFullModelRange().getEndPosition()) + editor?.setPosition(editor?.getModel()?.getFullModelRange()?.getEndPosition()) } } else { // console.debug(`expected uri: ${uri}, got: ${params.uri}`) diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index 77cc599..c047bac 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -12,7 +12,6 @@ import { store } from '../state/store'; import { useSelector } from 'react-redux'; import { useTranslation } from 'react-i18next'; import { t } from 'i18next'; -import { WorldLevelIdContext } from './infoview/context'; import { NavButton } from './navigation'; import { LoadingIcon } from './utils'; @@ -37,16 +36,24 @@ const InventoryContext = createContext<{ /** */ -function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, recent=false }) { +function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc } : + { item: InventoryTile, + name: any, + displayName: any, + locked: any, + disabled: any, + newly: any, + showDoc: any + }) { const icon = locked ? : - disabled ? : item.st + disabled ? : <> const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : "" // Note: This is somewhat a hack as the statement of lemmas comes currently in the form // `Namespace.statement_name (x y : Nat) : some type` const title = locked ? t("Not unlocked yet") : disabled ? t("Not available in this level") : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '') - const { gameId } = React.useContext(GameIdContext) + const { gameId, worldId, levelId } = React.useContext(GameIdContext) const difficulty = useSelector(selectDifficulty(gameId)) // local state to show checkmark after pressing the copy button @@ -67,7 +74,10 @@ function InventoryItem({item, name, displayName, locked, disabled, newly, showDo ev.stopPropagation() } - return
+ return
{icon} {displayName}
{copied ? : } @@ -92,7 +102,7 @@ function InventoryList({ items, tab=null, setTab=()=>{} } : const [categories, setCategories] = useState>([]) const [modifiedItems, setModifiedItems] = useState>([]) - const [recentItems, setRecentItems] = useState>([]) + const [currentWorldItems, setCurrentWorldItems] = useState>([]) useEffect(() => { @@ -111,7 +121,8 @@ function InventoryList({ items, tab=null, setTab=()=>{} } : let _modifiedItems : InventoryTile[] = items?.map(tile => inventory.includes(tile.name) ? {...tile, locked: false} : tile) setModifiedItems(_modifiedItems) // Item(s) proved in the preceeding level - setRecentItems(_modifiedItems.filter(x => x.world == worldId && x.level == levelId - 1)) + setCurrentWorldItems(_modifiedItems.filter(x => x.world == worldId && x.level < levelId)) + // setRecentItems(_modifiedItems.filter(x => x.world == worldId && x.level == levelId - 1)) }, [items, inventory]) @@ -120,7 +131,7 @@ function InventoryList({ items, tab=null, setTab=()=>{} } :
{categories.map((cat) => { let hasNew = modifiedItems.filter(item => item.new && (cat == item.category)).length > 0 - return
x.category).includes(cat) ? ' recent': ''}`} + return
x.category).includes(cat) ? ' recent': ''}`} onClick={() => { setTab(cat) }}>{cat}
})}
}
@@ -134,7 +145,6 @@ function InventoryList({ items, tab=null, setTab=()=>{} } : showDoc={() => {setDocTile(item)}} name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false} disabled={item.disabled} - recent={recentItems.map(x => x.name).includes(item.name)} newly={item.new} /> }) } @@ -155,7 +165,6 @@ export function Inventory () { /** Helper function to find if a list of tiles comprises any new elements. */ function containsNew(tiles: InventoryTile[]) { - console.log(tiles) return tiles?.filter(item => item.new).length > 0 } diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index 42a3649..49410f3 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -59,7 +59,7 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { {data.languages.map((lang) => ( - + ))} diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 0a61790..c392869 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 { faHome, faArrowRight } from '@fortawesome/free-solid-svg-icons' +import { faHome, faArrowRight, faCode, faTerminal } 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' @@ -17,6 +17,7 @@ import { EditorContext } from '../../../node_modules/lean4-infoview/src/infoview import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-infoview/src/infoview/editorConnection' import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event' import { Diagnostic } from 'vscode-languageserver-types' +import { DiagnosticSeverity } from 'vscode-languageclient'; import { GameIdContext } from '../app' import { useAppDispatch, useAppSelector } from '../hooks' @@ -27,12 +28,13 @@ import { store } from '../state/store' import { Button } from './button' import Markdown from './markdown' import {InventoryPanel} from './inventory' -import { hasInteractiveErrors } from './infoview/typewriter' -import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, - ProofContext, SelectionContext, WorldLevelIdContext, PageContext } from './infoview/context' -import { DualEditor } from './infoview/main' +import { Editor } from './editor' +import { Typewriter } from './typewriter' +import { ChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, + ProofContext, PageContext } from './infoview/context' +import { DualEditor, ExerciseStatement } from './infoview/main' import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api' -import { DeletedHints, Hint, Hints, MoreHelpButton, filterHints } from './hints' +import { DeletedHints, Hints, MoreHelpButton } from './hints' import path from 'path'; import '@fontsource/roboto/300.css' @@ -54,14 +56,14 @@ import { PreferencesPopup } from './popup/preferences' import { useTranslation } from 'react-i18next' import i18next from 'i18next' import { ChatButtons } from './chat' +import { NavButton } from './navigation' monacoSetup() export function Level({visible = true}) { - // const params = useParams() - // const levelId = parseInt(params.levelId) - // const worldId = params.worldId + let { t } = useTranslation() + const {gameId, worldId, levelId} = React.useContext(GameIdContext) @@ -71,153 +73,9 @@ export function Level({visible = true}) { }) const gameInfo = useGetGameInfoQuery({game: gameId}) + const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) - // pop-ups - const [impressum, setImpressum] = React.useState(false) - const [privacy, setPrivacy] = React.useState(false) - const [info, setInfo] = React.useState(false) - const [preferencesPopup, setPreferencesPopup] = React.useState(false) - - function closeImpressum() {setImpressum(false)} - function closePrivacy() {setPrivacy(false)} - function closeInfo() {setInfo(false)} - function closePreferencesPopup() {setPreferencesPopup(false)} - function toggleImpressum() {setImpressum(!impressum)} - function toggleInfo() {setInfo(!info)} - function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)} - - useEffect(() => {}, []) - - return
- - - -
-} - -function ChatPanel({lastLevel, visible = true}) { - let { t } = useTranslation() - const chatRef = useRef(null) - const {mobile} = useContext(PreferencesContext) - const {gameId} = useContext(GameIdContext) - const {worldId, levelId} = useContext(WorldLevelIdContext) - const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) - const {proof, setProof} = useContext(ProofContext) - const {deletedChat, setDeletedChat, showHelp, setShowHelp} = useContext(DeletedChatContext) - const {selectedStep, setSelectedStep} = useContext(SelectionContext) - const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) - - let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0 - - function toggleSelection(line: number) { - return (ev) => { - console.debug('toggled selection') - if (selectedStep == line) { - setSelectedStep(undefined) - } else { - setSelectedStep(line) - } - } - } - - useEffect(() => { - // TODO: For some reason this is always called twice - console.debug('scroll chat') - if (!mobile) { - chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0) - } - }, [proof, showHelp]) - - // Scroll to element if selection changes - useEffect(() => { - if (typeof selectedStep !== 'undefined') { - Array.from(chatRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => { - elem.scrollIntoView({block: "center"}) - }) - } - }, [selectedStep]) - - // useEffect(() => { - // // // Scroll to top when loading a new level - // // // TODO: Thats the wrong behaviour probably - // // chatRef.current!.scrollTo(0,0) - // }, [gameId, worldId, levelId]) - - let introText: Array = t(level?.data?.introduction, {ns: gameId}).split(/\n(\s*\n)+/) - - return
-
- {introText?.filter(t => t.trim()).map(((t, i) => - // Show the level's intro text as hints, too - - ))} - {proof?.steps.map((step, i) => { - let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints) - if (step.goals.length > 0 && !isLastStepWithErrors(proof, i)) { - return - } - })} - - {/* {modifiedHints.map((step, i) => { - // It the last step has errors, it will have the same hints - // as the second-to-last step. Therefore we should not display them. - if (!(i == proof?.steps.length - 1 && withErr)) { - // TODO: Should not use index as key. - return - } - })} */} - - {proof?.completed && - <> -
- {t("Level completed! 🎉")} -
- {level?.data?.conclusion?.trim() && -
- {t(level?.data?.conclusion, {ns: gameId})} -
- } - - } -
-
- {proof?.completed && (lastLevel ? - : - ) - } - -
-
-} - - -export function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject, visible?: boolean}) { - const {gameId} = React.useContext(GameIdContext) - const {worldId, levelId} = useContext(WorldLevelIdContext) - const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) - const gameInfo = useGetGameInfoQuery({game: gameId}) - return
-
- -
-
-} - -export function PlayableLevel() { - let { t } = useTranslation() const codeviewRef = useRef(null) - const {gameId} = React.useContext(GameIdContext) - const {worldId, levelId} = useContext(WorldLevelIdContext) - const {mobile} = React.useContext(PreferencesContext) const dispatch = useAppDispatch() @@ -227,20 +85,9 @@ export function PlayableLevel() { const typewriterMode = useSelector(selectTypewriterMode(gameId)) const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode})) - const gameInfo = useGetGameInfoQuery({game: gameId}) - const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) - - // The state variables for the `ProofContext` - const [proof, setProof] = useState({steps: [], diagnostics: [], completed: false, completedWithWarnings: false}) - const [interimDiags, setInterimDiags] = useState>([]) - const [isCrashed, setIsCrashed] = useState(false) - + const {deletedChat, setDeletedChat,showHelp, setShowHelp} = useContext(ChatContext) + const {proof, setProof} = useContext(ProofContext) - // 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 - const [deletedChat, setDeletedChat] = useState>([]) - // A set of row numbers where help is displayed - const [showHelp, setShowHelp] = useState>(new Set()) // Only for mobile layout const {page, setPage} = useContext(PageContext) @@ -259,8 +106,6 @@ export function PlayableLevel() { const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null) function closeInventoryDoc () {setInventoryDoc(null)} - - const onDidChangeContent = (code) => { dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code})) } @@ -309,7 +154,7 @@ export function PlayableLevel() { useEffect (() => { // Lock editor mode - if (level?.data?.template) { + if (levelInfo.data?.template) { setLockEditorMode(true) if (editor) { @@ -325,12 +170,12 @@ export function PlayableLevel() { // TODO: It does seem that the template is always indented by spaces. // This is a hack, assuming there are exactly two. if (!code.join('').trim().length) { - console.debug(`inserting template:\n${level.data.template}`) + console.debug(`inserting template:\n${levelInfo.data.template}`) // TODO: This does not work! HERE // Probably overwritten by a query to the server editor.executeEdits("template-writer", [{ range: editor.getModel().getFullModelRange(), - text: level.data.template + `\n`, + text: levelInfo.data.template + `\n`, forceMoveMarkers: true }]) } else { @@ -340,7 +185,7 @@ export function PlayableLevel() { } else { setLockEditorMode(false) } - }, [level, levelId, worldId, gameId, editor]) + }, [levelInfo, levelId, worldId, gameId, editor]) useEffect(() => { @@ -407,104 +252,346 @@ export function PlayableLevel() { } }, [editor, typewriterMode, lockEditorMode, onigasmH == null]) - return <> -
- - - - - - - {/* */} - - - - - - - - -} - // - // - // - // - -function IntroductionPanel({gameInfo}) { - let { t } = useTranslation() - const {gameId} = React.useContext(GameIdContext) - const {worldId} = useContext(WorldLevelIdContext) - const {mobile} = React.useContext(PreferencesContext) - - let text: Array = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).split(/\n(\s*\n)+/) - - return
-
- {text?.filter(t => t.trim()).map(((t, i) => - - ))} -
- + return
+ {/*
*/} + + + {levelId > 0 && + } + +
} -export default Level - -/** The site with the introduction text of a world */ -function Introduction() { +export function LevelWrapper({visible = true}) { let { t } = useTranslation() + const {gameId, worldId, levelId} = React.useContext(GameIdContext) - const {gameId} = React.useContext(GameIdContext) - const {mobile} = useContext(PreferencesContext) + // Load the namespace of the game + i18next.loadNamespaces(gameId).catch(err => { + console.warn(`translations for ${gameId} do not exist.`) + }) - const inventory = useLoadInventoryOverviewQuery({game: gameId}) - const gameInfo = useGetGameInfoQuery({game: gameId}) + const { mobile } = useContext(PreferencesContext) - const {worldId} = useContext(WorldLevelIdContext) + const gameInfo = useGetGameInfoQuery({game: gameId}) + const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) let image: string = gameInfo.data?.worlds.nodes[worldId].image + const codeviewRef = useRef(null) + const proofPanelRef = React.useRef(null) + + // set to true to prevent switching between typewriter and editor + const [lockEditorMode, setLockEditorMode] = useState(false) + const [typewriterInput, setTypewriterInput] = useState("") + const lastLevel = levelId >= gameInfo.data?.worldSize[worldId] + + // // impressum pop-up + // function toggleImpressum() {setImpressum(!impressum)} + // function togglePrivacy() {setPrivacy(!privacy)} + + // When clicking on an inventory item, the inventory is overlayed by the item's doc. + // If this state is set to a pair `(name, type)` then the according doc will be open. + // Set `inventoryDoc` to `null` to close the doc + const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null) + function closeInventoryDoc () {setInventoryDoc(null)} + - // const toggleImpressum = () => { - // setImpressum(!impressum) - // } - // const togglePrivacy = () => { - // setPrivacy(!privacy) - // } - return <> - {/* */} - {gameInfo.isLoading ? -
- : mobile ? - - : - // - // -
- {image && - - } + const dispatch = useAppDispatch() + + const typewriterMode = useSelector(selectTypewriterMode(gameId)) + const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode})) + + const initialCode = useAppSelector(selectCode(gameId, worldId, levelId)) + const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId)) + + + const onDidChangeContent = (code) => { + dispatch(codeEdited({game: gameId, world: worldId, level: levelId, code})) + } + + const onDidChangeSelection = (monacoSelections) => { + const selections = monacoSelections.map( + ({selectionStartLineNumber, selectionStartColumn, positionLineNumber, positionColumn}) => + {return {selectionStartLineNumber, selectionStartColumn, positionLineNumber, positionColumn}}) + dispatch(changedSelection({game: gameId, world: worldId, level: levelId, selections})) + } + + + useEffect(() => { + console.info(`Loading Level: ${mobile}`) + }, [mobile, gameId, worldId, levelId]) + + // const {editor, infoProvider, editorConnection} = + // useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) + + + + /** toggle input mode if allowed */ + function toggleInputMode(ev: React.MouseEvent) { + if (!lockEditorMode) { + setTypewriterMode(!typewriterMode) + console.log('test') + } + } + + // { typewriterMode ? : } + + // + // + return
+ { image && +
+ +
+ } + { levelId > 0 && +
+ toggleInputMode(ev)} + title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")} /> +
+
+ + + {/* { typewriterMode ? : } */}
- // {/* */} - // + +
} - +
+} + +// +// + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +// function ChatPanel({lastLevel, visible = true}) { +// let { t } = useTranslation() +// const chatRef = useRef(null) +// const {mobile} = useContext(PreferencesContext) +// const {gameId, worldId, levelId} = useContext(GameIdContext) +// const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) +// const {proof, setProof} = useContext(ProofContext) +// const {deletedChat, setDeletedChat, showHelp, setShowHelp} = useContext(DeletedChatContext) +// const {selectedStep, setSelectedStep} = useContext(SelectionContext) +// const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) + +// let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0 + +// function toggleSelection(line: number) { +// return (ev) => { +// console.debug('toggled selection') +// if (selectedStep == line) { +// setSelectedStep(undefined) +// } else { +// setSelectedStep(line) +// } +// } +// } + +// useEffect(() => { +// // TODO: For some reason this is always called twice +// console.debug('scroll chat') +// if (!mobile) { +// chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0) +// } +// }, [proof, showHelp]) + +// // Scroll to element if selection changes +// useEffect(() => { +// if (typeof selectedStep !== 'undefined') { +// Array.from(chatRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => { +// elem.scrollIntoView({block: "center"}) +// }) +// } +// }, [selectedStep]) + +// // useEffect(() => { +// // // // Scroll to top when loading a new level +// // // // TODO: Thats the wrong behaviour probably +// // // chatRef.current!.scrollTo(0,0) +// // }, [gameId, worldId, levelId]) + +// let introText: Array = t(level?.data?.introduction, {ns: gameId}).split(/\n(\s*\n)+/) + +// return
+//
+// {introText?.filter(t => t.trim()).map(((t, i) => +// // Show the level's intro text as hints, too +// +// ))} +// {proof?.steps.map((step, i) => { +// let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints) +// if (step.goals.length > 0 && !isLastStepWithErrors(proof, i)) { +// return +// } +// })} + +// {/* {modifiedHints.map((step, i) => { +// // It the last step has errors, it will have the same hints +// // as the second-to-last step. Therefore we should not display them. +// if (!(i == proof?.steps.length - 1 && withErr)) { +// // TODO: Should not use index as key. +// return +// } +// })} */} +// +// {proof?.completed && +// <> +//
+// {t("Level completed! 🎉")} +//
+// {level?.data?.conclusion?.trim() && +//
+// {t(level?.data?.conclusion, {ns: gameId})} +//
+// } +// +// } +//
+//
+// {proof?.completed && (lastLevel ? +// : +// ) +// } +// +//
+//
+// } + + +export function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject, visible?: boolean}) { + const {gameId, worldId, levelId} = React.useContext(GameIdContext) + const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) + const gameInfo = useGetGameInfoQuery({game: gameId}) + return
+
+ +
+
} + + // + // + // + // + +// function IntroductionPanel({gameInfo}) { +// let { t } = useTranslation() +// const {gameId, worldId} = React.useContext(GameIdContext) +// const {mobile} = React.useContext(PreferencesContext) + +// let text: Array = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).split(/\n(\s*\n)+/) + +// return
+//
+// {text?.filter(t => t.trim()).map(((t, i) => +// +// ))} +//
+// +//
+// } + +// /** The site with the introduction text of a world */ +// function Introduction() { +// let { t } = useTranslation() + +// const {gameId, worldId} = React.useContext(GameIdContext) +// const {mobile} = useContext(PreferencesContext) + +// const inventory = useLoadInventoryOverviewQuery({game: gameId}) + +// const gameInfo = useGetGameInfoQuery({game: gameId}) + + +// let image: string = gameInfo.data?.worlds.nodes[worldId].image + + +// // const toggleImpressum = () => { +// // setImpressum(!impressum) +// // } +// // const togglePrivacy = () => { +// // setPrivacy(!privacy) +// // } +// return <> +// {/* */} +// {gameInfo.isLoading ? +//
+// : mobile ? +// +// : +// // +// // +//
+// {image && +// +// } + +//
+// // {/* */} +// // +// } + +// +// } + // {mobile? // // TODO: This is copied from the `Split` component below... // <> @@ -530,8 +617,7 @@ function Introduction() { function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) { - const {gameId} = React.useContext(GameIdContext) - const {worldId, levelId} = useContext(WorldLevelIdContext) + const {gameId, worldId, levelId} = React.useContext(GameIdContext) const [editor, setEditor] = useState(null) const [infoProvider, setInfoProvider] = useState(null) @@ -544,6 +630,9 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange const difficulty: number = useSelector(selectDifficulty(gameId)) useEffect(() => { + // monaco.editor.getModels().forEach(model => model.dispose()); + + console.info(`trying to create model: ${gameId} ${worldId} ${levelId} ${uri}`) const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri) if (onDidChangeContent) { model.onDidChangeContent(() => onDidChangeContent(model.getValue())) diff --git a/client/src/components/navigation.tsx b/client/src/components/navigation.tsx index 522b74b..0cf3832 100644 --- a/client/src/components/navigation.tsx +++ b/client/src/components/navigation.tsx @@ -12,7 +12,7 @@ import { useTranslation } from 'react-i18next' import '../css/navigation.css' import { PopupContext } from './popup/popup' import { useSelector } from 'react-redux' -import { selectCompleted, selectDifficulty, selectProgress } from '../state/progress' +import { selectCompleted, selectDifficulty, selectProgress, selectReadIntro } from '../state/progress' import lean4gameConfig from '../config.json' import { Flag } from './flag' import { useAppSelector } from '../hooks' @@ -34,8 +34,9 @@ export const NavButton: React.FC<{ href?: string inverted?: boolean disabled?: boolean -}> = ({icon, iconElement, text, onClick=()=>{}, title, href=null, inverted=false, disabled=false}) => { - return + className?: string +}> = ({icon, iconElement, text, onClick=()=>{}, title, href=null, inverted=false, disabled=false, className=''}) => { + return {iconElement ?? (icon && )}{text && <> {text}} } @@ -82,6 +83,9 @@ function MobileNavigationOverview () { const {page, setPage} = useContext(PageContext) const { setPopupContent } = useContext(PopupContext) + const { gameId, worldId } = useContext(GameIdContext) + const readIntro = useSelector(selectReadIntro(gameId, worldId)) + return
setPage(page+1)} + disabled={!readIntro} inverted={true} /> }
@@ -123,13 +128,7 @@ function DesktopNavigationLevel () { const difficulty = useSelector(selectDifficulty(gameId)) const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) - /** toggle input mode if allowed */ - function toggleInputMode(ev: React.MouseEvent) { - if (!lockEditorMode) { - setTypewriterMode(!typewriterMode) - console.log('test') - } - } + const readIntro = useSelector(selectReadIntro(gameId, worldId)) const worldTitle = gameInfo.data?.worlds.nodes[worldId]?.title const levelTitle = ((levelId == 0) ? @@ -166,22 +165,14 @@ function DesktopNavigationLevel () { icon={faHome} text={t("Leave World")} inverted={true} - disabled={difficulty == 0 || !completed} + disabled={levelId > 0 && difficulty == 2 && !completed} href={`#/${gameId}`} /> : } - { levelId > 0 && - toggleInputMode(ev)} - title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")} /> - }
} @@ -228,6 +219,8 @@ export function Navigation () { const difficulty = useSelector(selectDifficulty(gameId)) const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) + const readIntro = useSelector(selectReadIntro(gameId, worldId)) + const [navOpen, setNavOpen] = useState(false) const [langNavOpen, setLangNavOpen] = useState(false) function toggleNav () {setNavOpen(!navOpen); setLangNavOpen(false)} @@ -280,6 +273,7 @@ export function Navigation () { // Show all languages the game is available in gameInfo.data?.tile?.languages.map(iso => } text={lean4gameConfig.newLanguages[iso]?.name} onClick={() => {setLanguage(iso)}} @@ -287,6 +281,7 @@ export function Navigation () { // Show all languages the interface is available in (e.g. landing page) Object.entries(lean4gameConfig.newLanguages).map(([iso, val]) => } text={lean4gameConfig.newLanguages[iso]?.name} onClick={() => {setLanguage(iso)}} @@ -302,12 +297,12 @@ export function Navigation () { icon={faHome} text={t("Leave World")} inverted={true} - disabled={difficulty == 0 || !completed} + disabled={levelId > 0 && difficulty == 2 && !completed} href={`#/${gameId}`} /> : )} {mobile && levelId > 0 && diff --git a/client/src/components/popup/popup.tsx b/client/src/components/popup/popup.tsx index d856c4b..10576f5 100644 --- a/client/src/components/popup/popup.tsx +++ b/client/src/components/popup/popup.tsx @@ -48,9 +48,9 @@ export function Popup () { return
- + inverted={true} /> */}
{Popups[popupContent]}
diff --git a/client/src/components/typewriter.tsx b/client/src/components/typewriter.tsx new file mode 100644 index 0000000..5df949e --- /dev/null +++ b/client/src/components/typewriter.tsx @@ -0,0 +1,7 @@ +import * as React from 'react' + +export function Typewriter () { + return

+ I'm a typewriter +

+} diff --git a/client/src/components/welcome.tsx b/client/src/components/welcome.tsx index 84bcb9e..fb6a80e 100644 --- a/client/src/components/welcome.tsx +++ b/client/src/components/welcome.tsx @@ -7,7 +7,7 @@ import { faArrowRight } from '@fortawesome/free-solid-svg-icons' import { GameIdContext } from '../app' import { useAppDispatch, useAppSelector } from '../hooks' -import { changedOpenedIntro, selectOpenedIntro } from '../state/progress' +import { changedReadIntro, selectReadIntro } from '../state/progress' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api' import { Button } from './button' import { PageContext, PreferencesContext } from './infoview/context' @@ -55,7 +55,7 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string, @@ -66,7 +66,7 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string, /** main page of the game showing among others the tree of worlds/levels */ function Welcome() { - const {gameId} = React.useContext(GameIdContext) + const {gameId, worldId} = React.useContext(GameIdContext) // Load the namespace of the game i18next.loadNamespaces(gameId) @@ -78,13 +78,13 @@ function Welcome() { const inventory = useLoadInventoryOverviewQuery({game: gameId}) // For mobile only - const openedIntro = useAppSelector(selectOpenedIntro(gameId)) + const readIntro = useAppSelector(selectReadIntro(gameId, worldId)) const {page, setPage} = React.useContext(PageContext) - // TODO: recover `openedIntro` functionality + // TODO: recover `readIntro` functionality - // const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0) + // const [pageNumber, setPageNumber] = React.useState(readIntro ? 1 : 0) // pop-ups const [eraseMenu, setEraseMenu] = React.useState(false) diff --git a/client/src/components/world_tree.tsx b/client/src/components/world_tree.tsx index 636a1a6..f4d6361 100644 --- a/client/src/components/world_tree.tsx +++ b/client/src/components/world_tree.tsx @@ -197,47 +197,6 @@ export const downloadFile = ({ data, fileName, fileType } : a.remove() } -/** The menu that is shown next to the world selection graph */ -export function WorldSelectionMenu({rulesHelp, setRulesHelp}) { - const { t, i18n } = useTranslation() - const {gameId} = React.useContext(GameIdContext) - const difficulty = useSelector(selectDifficulty(gameId)) - const dispatch = useAppDispatch() - const { mobile } = React.useContext(PreferencesContext) - - - function label(x : number) { - return x == 0 ? t("none") : x == 1 ? t("relaxed") : t("regular") - } - - - return -} - export function computeWorldLayout(worlds) { let elements = [] for (let id in worlds.nodes) { @@ -360,7 +319,7 @@ export function WorldTreePanel ({visible = true}) { let dx = bounds ? s*(bounds.x2 - bounds.x1) + 2*padding : null - return
+ return
{/* */} { gameInfo.data ? *:not(:last-child) { + /* display: block; */ + margin-right: .2rem; +} + +.button-row .btn-placeholder { + display: inline-block; + flex: 1; + margin: 0; +} diff --git a/client/src/css/game.css b/client/src/css/game.css index 1d12a9c..9dc2ee2 100644 --- a/client/src/css/game.css +++ b/client/src/css/game.css @@ -23,6 +23,11 @@ .column { width: 100%; + height: 100%; + overflow: auto; + position: relative; + scroll-behavior: smooth; + } .slider .column { diff --git a/client/src/css/infoview.css b/client/src/css/infoview.css index dfb76ea..1d3428b 100644 --- a/client/src/css/infoview.css +++ b/client/src/css/infoview.css @@ -70,13 +70,6 @@ flex-direction: column; } -.typewriter-interface .proof .MuiCircularProgress-root { - left: 50%; - position: relative; - margin-left: -20px; - margin-bottom: 0.6em; -} - .typewriter .typewriter-input { flex: 1; } @@ -143,22 +136,12 @@ } -/* Push the goals to the bottom for now, until we insert the proof history above. */ -.typewriter-interface .content { - display: flex; - flex-direction: column; - scroll-behavior: smooth; -} /* TODO this is in the wrong file */ .chat { scroll-behavior: smooth; } -.typewriter-interface .content .tmp-pusher { - flex: 1; -} - .exercise .command { background-color: #bbb; padding: .5em; diff --git a/client/src/css/inventory.css b/client/src/css/inventory.css index ee8bf0b..7ecd134 100644 --- a/client/src/css/inventory.css +++ b/client/src/css/inventory.css @@ -46,9 +46,14 @@ background-color: rgb(255, 242, 190); } +.inventory .item.current-world { + background-color: rgb(250, 231, 255); +} + .inventory .item.recent { background-color: rgb(242, 190, 255); } + .inventory .item:not(.locked), .inventory .item.enabled { cursor: pointer; } diff --git a/client/src/css/level.css b/client/src/css/level.css index 0ba6731..f5726d4 100644 --- a/client/src/css/level.css +++ b/client/src/css/level.css @@ -5,12 +5,12 @@ /* display: flex; */ } -.inventory-panel, .exercise-panel, .doc-panel, .introduction-panel { +/* .inventory-panel, .exercise-panel, .doc-panel, .introduction-panel { height: 100%; width: 100%; overflow: auto; position: relative; -} +} */ .infoview { padding-top: 1em; @@ -44,11 +44,11 @@ padding-top: 0em; } -.exercise { +/* .exercise { flex: 1 1 auto; display: flex; flex-flow: column; -} +} */ .codeview { flex: 1 1 auto; @@ -216,12 +216,6 @@ td code { padding: .5em; } -/* .exercise-panel { - display: flex; - flex-flow: column; - height: 100%; -} */ - /* .button-row.mobile { margin: .5rem; padding-top: .2rem; @@ -236,17 +230,18 @@ td code { } */ -.typewriter-interface { +.exercise-content { display: flex; flex-flow: column; height: 100%; + z-index: 1; } .typewriter { flex: 0 1 auto; } -.typewriter-interface .content { +.exercise-content { flex: 1 1 auto; overflow-y: scroll; padding: 0; @@ -332,22 +327,31 @@ td code { justify-content: center; } -.typewriter-interface .content, .world-image-container.empty { +.exercise { background-color: #eee; + position: relative; } -.world-image-container { +.world-image { + height: 100%; + width: 100%; + overflow: hidden; display: flex; flex-direction: column; - min-height: 0px; /* somehow this has a desired affect, but why? */ - overflow: hidden; + position: absolute; + z-index: 0; + /* min-height: 0px;*/ /* somehow this has a desired affect, but why? */ } -.world-image-container img.contain { +.world-image img.contain { + height: 100%; + width: 100%; object-fit: contain; + object-position: top center; + pointer-events: none; } -.world-image-container.center { +.world-image.center { justify-content: center; } @@ -357,10 +361,33 @@ td code { object-fit: cover; } -.typewriter-interface .proof { +.proof { + z-index: 2; background-color: #fff; } +.exercise-content .tmp-pusher { + flex: 1; +} + +.exercise-content { + background: none; +} + +/* Push the goals to the bottom for now, until we insert the proof history above. */ +.exercise-content { + display: flex; + flex-direction: column; + scroll-behavior: smooth; +} + +.exercise-content .proof .MuiCircularProgress-root { + left: 50%; + position: relative; + margin-left: -20px; + margin-bottom: 0.6em; +} + .toggle-width { min-width: 40px; text-align: center; diff --git a/client/src/css/navigation.css b/client/src/css/navigation.css index 569f445..698720b 100644 --- a/client/src/css/navigation.css +++ b/client/src/css/navigation.css @@ -75,3 +75,23 @@ nav { .dropdown .svg-inline--fa { width: 1.8rem; } + +.btn-right { + float: right; + margin: 0.2rem; +} + +.btn-input-mode { + position: absolute; + right: 0.4rem; + z-index: 5; + top: 0.4rem; + margin: 0; + border: 1px solid var(--clr-primary); + background-color: #eee; + font-size: .7rem; + /* box-shadow: .0em .0em .4em .1em var(--clr-primary); */ + /* box-shadow: -.1rem .3rem .3rem 0 var(--clr-primary); */ + /* border-top-right-radius: 0; + border-bottom-right-radius: 0; */ +} diff --git a/client/src/index.tsx b/client/src/index.tsx index 3aa7f08..2cf228b 100644 --- a/client/src/index.tsx +++ b/client/src/index.tsx @@ -8,7 +8,6 @@ import { createHashRouter, RouterProvider, Route, redirect } from "react-router- import ErrorPage from './components/error_page' import Welcome from './components/welcome' import LandingPage from './components/landing_page' -import Level from './components/level' import './i18n'; import Game from './components/game' diff --git a/client/src/state/api.ts b/client/src/state/api.ts index 5dabdba..71ddec7 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -85,7 +85,7 @@ export const apiSlice = createApi({ }), loadLevel: builder.query({ query: ({game, world, level}) => { - if (world) { + if (world && level > 0) { return `${game}/level__${world}__${level}.json` } else { return `${game}/inventory.json` diff --git a/client/src/state/progress.ts b/client/src/state/progress.ts index 2922eaf..191244f 100644 --- a/client/src/state/progress.ts +++ b/client/src/state/progress.ts @@ -19,13 +19,13 @@ interface LevelProgressState { help: number[], // A set of rows where hidden hints have been displayed } interface WorldProgressState { - [world: string] : {[level: number]: LevelProgressState}, + [world: string] : {[level: number]: LevelProgressState, readIntro: boolean}, } export interface GameProgressState { inventory: string[], difficulty: number, - openedIntro: boolean, + readIntro: boolean, data: WorldProgressState, typewriterMode?: boolean } @@ -54,19 +54,24 @@ const initalLevelProgressState: LevelProgressState = {code: "", completed: false /** Add an empty skeleton with progress for the current game */ function addGameProgress (state: ProgressState, action: PayloadAction<{game: string}>) { if (!state.games[action.payload.game.toLowerCase()]) { - state.games[action.payload.game.toLowerCase()] = {inventory: [], openedIntro: false, data: {}, difficulty: DEFAULT_DIFFICULTY} + state.games[action.payload.game.toLowerCase()] = {inventory: [], readIntro: false, data: {}, difficulty: DEFAULT_DIFFICULTY} } if (!state.games[action.payload.game.toLowerCase()].data) { state.games[action.payload.game.toLowerCase()].data = {} } } -/** Add an empty skeleton with progress for the current level */ -function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) { +function addWorldProgress(state: ProgressState, action: PayloadAction<{game: string, world: string}>) { addGameProgress(state, action) if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world]) { - state.games[action.payload.game.toLowerCase()].data[action.payload.world] = {} + state.games[action.payload.game.toLowerCase()].data[action.payload.world] = {readIntro: false} } +} + +/** Add an empty skeleton with progress for the current level */ +function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) { + addGameProgress(state, action) + addWorldProgress(state, action) if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level]) { state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level] = {...initalLevelProgressState} } @@ -80,7 +85,7 @@ export const progressSlice = createSlice({ codeEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, code: string}>) { addLevelProgress(state, action) state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].code = action.payload.code - state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = false + // state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = false }, /** TODO: docstring */ changedSelection(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, selections: Selection[]}>) { @@ -100,7 +105,7 @@ export const progressSlice = createSlice({ }, /** delete all progress for this game */ deleteProgress(state: ProgressState, action: PayloadAction<{game: string}>) { - state.games[action.payload.game.toLowerCase()] = {inventory: [], data: {}, openedIntro: false, difficulty: DEFAULT_DIFFICULTY} + state.games[action.payload.game.toLowerCase()] = {inventory: [], data: {}, readIntro: false, difficulty: DEFAULT_DIFFICULTY} }, /** delete progress for this level */ deleteLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) { @@ -123,9 +128,13 @@ export const progressSlice = createSlice({ state.games[action.payload.game.toLowerCase()].difficulty = action.payload.difficulty }, /** set the difficulty */ - changedOpenedIntro(state: ProgressState, action: PayloadAction<{game: string, openedIntro: boolean}>) { - addGameProgress(state, action) - state.games[action.payload.game.toLowerCase()].openedIntro = action.payload.openedIntro + changedReadIntro(state: ProgressState, action: PayloadAction<{game: string, world: string, readIntro: boolean}>) { + addWorldProgress(state, action) + if (action.payload.world) { + state.games[action.payload.game.toLowerCase()].data[action.payload.world].readIntro = action.payload.readIntro + } else { + state.games[action.payload.game.toLowerCase()].readIntro = action.payload.readIntro + } }, /** set the typewriter mode */ changeTypewriterMode(state: ProgressState, action: PayloadAction<{game: string, typewriterMode: boolean}>) { @@ -137,47 +146,47 @@ export const progressSlice = createSlice({ /** if the level does not exist, return default values */ export function selectLevel(game: string, world: string, level: number) { - return (state) =>{ - if (!state.progress.games[game.toLowerCase()]) { return initalLevelProgressState } - if (!state.progress.games[game.toLowerCase()].data[world]) { return initalLevelProgressState } - if (!state.progress.games[game.toLowerCase()].data[world][level]) { return initalLevelProgressState } - return state.progress.games[game.toLowerCase()].data[world][level] + return (state) => { + if (!state.progress.games[game?.toLowerCase()]) { return initalLevelProgressState } + if (!state.progress.games[game?.toLowerCase()].data[world]) { return initalLevelProgressState } + if (!state.progress.games[game?.toLowerCase()].data[world][level]) { return initalLevelProgressState } + return state.progress.games[game?.toLowerCase()].data[world][level] } } /** return the code of the current level */ export function selectCode(game: string, world: string, level: number) { return (state) => { - return selectLevel(game.toLowerCase(), world, level)(state).code + return selectLevel(game?.toLowerCase(), world, level)(state).code } } /** return the current inventory */ export function selectInventory(game: string) { return (state) => { - if (!state.progress.games[game.toLowerCase()]) { return [] } - return state.progress.games[game.toLowerCase()].inventory + if (!state.progress.games[game?.toLowerCase()]) { return [] } + return state.progress.games[game?.toLowerCase()].inventory } } /** return the code of the current level */ export function selectHelp(game: string, world: string, level: number) { return (state) => { - return selectLevel(game.toLowerCase(), world, level)(state).help + return selectLevel(game?.toLowerCase(), world, level)(state).help } } /** return the selections made in the current level */ export function selectSelections(game: string, world: string, level: number) { return (state) => { - return selectLevel(game.toLowerCase(), world, level)(state).selections + return selectLevel(game?.toLowerCase(), world, level)(state).selections } } /** return whether the current level is clompleted */ export function selectCompleted(game: string, world: string, level: number) { return (state) => { - return selectLevel(game.toLowerCase(), world, level)(state).completed + return selectLevel(game?.toLowerCase(), world, level)(state).completed } } @@ -191,14 +200,17 @@ export function selectProgress(game: string) { /** return difficulty for the current game if it exists */ export function selectDifficulty(game: string) { return (state) => { - return state.progress.games[game.toLowerCase()]?.difficulty ?? DEFAULT_DIFFICULTY + return state.progress.games[game?.toLowerCase()]?.difficulty ?? DEFAULT_DIFFICULTY } } /** return whether the intro has been read */ -export function selectOpenedIntro(game: string) { +export function selectReadIntro(game: string, worldId: string) { return (state) => { - return state.progress.games[game?.toLowerCase()]?.openedIntro + if (worldId) { + return state.progress.games[game?.toLowerCase()].data[worldId]?.readIntro + } + return state.progress.games[game?.toLowerCase()]?.readIntro } } @@ -211,5 +223,5 @@ export function selectTypewriterMode(game: string) { /** Export actions to modify the progress */ export const { changedSelection, codeEdited, levelCompleted, deleteProgress, - deleteLevelProgress, loadProgress, helpEdited, changedInventory, changedOpenedIntro, + deleteLevelProgress, loadProgress, helpEdited, changedInventory, changedReadIntro, changedDifficulty, changeTypewriterMode} = progressSlice.actions