diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index 0c7e9e2..8756779 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -7,11 +7,8 @@ import '@fontsource/roboto/700.css'; import ReactMarkdown from 'react-markdown'; import { MathJax } from "better-react-mathjax"; import { Link as RouterLink } from 'react-router-dom'; - - import { Box, Button, CircularProgress, FormControlLabel, FormGroup, Switch } from '@mui/material'; import Grid from '@mui/material/Unstable_Grid2'; - import LeftPanel from './LeftPanel'; import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider'; import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter'; @@ -23,7 +20,6 @@ import './level.css' import { ConnectionContext } from '../connection'; import Infoview from './Infoview'; import { useParams } from 'react-router-dom'; -import { MonacoServices } from 'monaco-languageclient'; import { useLoadLevelQuery } from '../game/api'; @@ -34,9 +30,6 @@ function Level() { const levelId = parseInt(params.levelId) const worldId = params.worldId - const [editor, setEditor] = useState(null) - const [infoProvider, setInfoProvider] = useState(null) - const [infoviewApi, setInfoviewApi] = useState(null) const [expertInfoview, setExpertInfoview] = useState(false) const codeviewRef = useRef(null) @@ -50,6 +43,52 @@ function Level() { const connection = React.useContext(ConnectionContext) + const level = useLoadLevelQuery({world: worldId, level: levelId}) + + const {editor, infoProvider} = useLevelEditor(worldId, levelId, codeviewRef, infoviewRef) + + return <> + + + + + + +
+ {level?.data?.introduction} +
+
+
+
+ + + + + +
+
+ +
+ + { setExpertInfoview(!expertInfoview) }} control={} label="Expert mode" /> + +
+
+ +} + +export default Level + + +function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewRef) { + + const connection = React.useContext(ConnectionContext) + + const [editor, setEditor] = useState(null) + const [infoProvider, setInfoProvider] = useState(null) + const [infoviewApi, setInfoviewApi] = useState(null) + + // Create Editor useEffect(() => { const editor = monaco.editor.create(codeviewRef.current!, { glyphMargin: true, @@ -76,11 +115,9 @@ function Level() { setInfoProvider(infoProvider) setInfoviewApi(infoviewApi) - return () => { editor.dispose() } }, []) - - // The next function will be called when the level changes + // Create model when level changes useEffect(() => { connection.startLeanClient().then((leanClient) => { if (editor) { @@ -94,45 +131,10 @@ function Level() { infoProvider.openPreview(editor, infoviewApi) new AbbreviationRewriter(new AbbreviationProvider(), model, editor) - - - return () => { model.dispose(); } } }) }, [editor, levelId, connection]) - - const level = useLoadLevelQuery({world: worldId, level: levelId}) - - return <> - - - - - - -
- {level?.data?.introduction} -
-
-
-
- - - - - -
-
- -
- - { setExpertInfoview(!expertInfoview) }} control={} label="Expert mode" /> - -
-
- + return {editor, infoProvider} } - -export default Level