diff --git a/client/src/components/LeftPanel.tsx b/client/src/components/LeftPanel.tsx index b46ddb3..9457b38 100644 --- a/client/src/components/LeftPanel.tsx +++ b/client/src/components/LeftPanel.tsx @@ -71,12 +71,12 @@ function LemmaDocs({ lemmas }) { function LeftPanel({ spells, inventory }) { return ( - {spells.length > 0 && + {spells && spells.length > 0 && Spell book {spells.map((spell) => )} } - {inventory.length > 0 && } + {inventory && inventory.length > 0 && } ) } diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index e094771..0c7e9e2 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -9,7 +9,7 @@ import { MathJax } from "better-react-mathjax"; import { Link as RouterLink } from 'react-router-dom'; -import { Button, FormControlLabel, FormGroup, Switch } from '@mui/material'; +import { Box, Button, CircularProgress, FormControlLabel, FormGroup, Switch } from '@mui/material'; import Grid from '@mui/material/Unstable_Grid2'; import LeftPanel from './LeftPanel'; @@ -24,6 +24,7 @@ import { ConnectionContext } from '../connection'; import Infoview from './Infoview'; import { useParams } from 'react-router-dom'; import { MonacoServices } from 'monaco-languageclient'; +import { useLoadLevelQuery } from '../game/api'; @@ -33,43 +34,15 @@ function Level() { const levelId = parseInt(params.levelId) const worldId = params.worldId - const [tacticDocs, setTacticDocs] = useState([]) - const [lemmaDocs, setLemmaDocs] = useState([]) const [editor, setEditor] = useState(null) const [infoProvider, setInfoProvider] = useState(null) const [infoviewApi, setInfoviewApi] = useState(null) const [expertInfoview, setExpertInfoview] = useState(false) - - const [leanData, setLeanData] = useState({goals: []}) - const [history, setHistory] = useState([]) - const [lastTactic, setLastTactic] = useState("") - const [introduction, setIntroduction] = useState("") - const [errors, setErrors] = useState([]) const codeviewRef = useRef(null) const infoviewRef = useRef(null) const messagePanelRef = useRef(null) - const [ready, setReady] = useState(false) - - const [message, setMessage] = useState("") - const [messageOpen, setMessageOpen] = useState(false) - - - const [completed, setCompleted] = useState(false) - - const processResponse = (res:any) => { - setLeanData(res); - // setErrors(res.errors); - // if (res.message !== "" && res.errors?.length === 0) { - // setMessage(res.message) - // setMessageOpen(true) - // } - // if (res.goals?.length === 0 && res.errors?.length === 0) { - // setCompleted(true) - // } - } - useEffect(() => { // Scroll to top when loading a new level messagePanelRef.current!.scrollTo(0,0) @@ -106,57 +79,43 @@ function Level() { return () => { editor.dispose() } }, []) - const uri = `file:///${worldId}/${levelId}` // The next function will be called when the level changes useEffect(() => { connection.startLeanClient().then((leanClient) => { if (editor) { - const model = monaco.editor.createModel('', 'lean4', monaco.Uri.parse(uri)) + const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`) + const model = monaco.editor.getModel(uri) ?? + monaco.editor.createModel('', 'lean4', uri) editor.setModel(model) infoviewApi.serverRestarted(leanClient.initializeResult) infoProvider.openPreview(editor, infoviewApi) - setReady(true) new AbbreviationRewriter(new AbbreviationProvider(), model, editor) - leanClient.sendRequest("loadLevel", {world: worldId, level: levelId}).then((res) => { - // setLevelTitle("Level " + res["index"] + ": " + res["title"]) - // setIndex(parseInt(res["index"])) - setTacticDocs(res["tactics"]) - setLemmaDocs(res["lemmas"]) - setIntroduction(res["introduction"]) - processResponse(res) - }); - - return () => { model.dispose(); setReady(false) } + return () => { model.dispose(); } } }) }, [editor, levelId, connection]) - function loadLevel(index) { - setCompleted(false) - setHistory([]) - // setCurLevel(index) - } - return ( - + const level = useLoadLevelQuery({world: worldId, level: levelId}) + + return <> + + - + - {introduction} + {level?.data?.introduction} - {/* */} - {/* */} @@ -173,7 +132,7 @@ function Level() { - ) + > } export default Level diff --git a/client/src/game/api.ts b/client/src/game/api.ts index c23e18e..1e52fcd 100644 --- a/client/src/game/api.ts +++ b/client/src/game/api.ts @@ -1,7 +1,7 @@ import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react' import { Connection } from '../connection' -interface GameState { +interface GameInfo { title: null|string, introduction: null|string, worlds: null|{nodes: string[], edges: string[][2]}, @@ -9,6 +9,14 @@ interface GameState { conclusion: null|string, } +interface LevelInfo { + title: null|string, + introduction: null|string, + index: number, + tactics: any[], + lemmas: any[] +} + const customBaseQuery = async ( args : {method: string, params?: any}, { signal, dispatch, getState, extra }, @@ -27,12 +35,15 @@ export const gameApi = createApi({ reducerPath: 'gameApi', baseQuery: customBaseQuery, endpoints: (builder) => ({ - getGameInfo: builder.query({ + getGameInfo: builder.query({ query: () => {return {method: 'info', params: {}}}, }), + loadLevel: builder.query({ + query: ({world, level}) => {return {method: "loadLevel", params: {world, level}}}, + }), }), }) // Export hooks for usage in functional components, which are // auto-generated based on the defined endpoints -export const { useGetGameInfoQuery } = gameApi +export const { useGetGameInfoQuery, useLoadLevelQuery } = gameApi