diff --git a/client/src/App.tsx b/client/src/App.tsx index d43a626..67cfc92 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -1,8 +1,6 @@ import * as React from 'react'; import { useState, useEffect } from 'react'; import { MathJaxContext } from "better-react-mathjax"; -import * as rpc from 'vscode-ws-jsonrpc'; -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import { Outlet } from "react-router-dom"; import '@fontsource/roboto/300.css'; @@ -12,9 +10,6 @@ import '@fontsource/roboto/700.css'; import { AppBar, CssBaseline, Toolbar, Typography } from '@mui/material'; -import Welcome from './components/Welcome'; -import Level from './components/Level'; -import GoodBye from './components/GoodBye'; import { useAppSelector } from './hooks'; function App() { diff --git a/client/src/ErrorPage.tsx b/client/src/ErrorPage.tsx new file mode 100644 index 0000000..3dbeb62 --- /dev/null +++ b/client/src/ErrorPage.tsx @@ -0,0 +1,17 @@ +import * as React from 'react' +import { useRouteError } from "react-router-dom"; + +export default function ErrorPage() { + const error: any = useRouteError(); + console.error(error); + + return ( +
+

Oops!

+

Sorry, an unexpected error has occurred.

+

+ {error.statusText || error.message} +

+
+ ); +} diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index fc4c97e..6179c3a 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -6,6 +6,8 @@ import '@fontsource/roboto/500.css'; 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 { Button, FormControlLabel, FormGroup, Switch } from '@mui/material'; import Grid from '@mui/material/Unstable_Grid2'; @@ -20,10 +22,16 @@ import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import './level.css' import { ConnectionContext } from '../connection'; import Infoview from './Infoview'; +import { useParams } from 'react-router-dom'; +import { MonacoServices } from 'monaco-languageclient'; + + function Level() { - const level = 1 - const [index, setIndex] = useState(level) // Level number + + const params = useParams(); + const levelId = parseInt(params.levelId) + const [tacticDocs, setTacticDocs] = useState([]) const [lemmaDocs, setLemmaDocs] = useState([]) const [editor, setEditor] = useState(null) @@ -64,7 +72,7 @@ function Level() { useEffect(() => { // Scroll to top when loading a new level messagePanelRef.current!.scrollTo(0,0) - }, [level]) + }, [levelId]) const connection = React.useContext(ConnectionContext) @@ -97,12 +105,13 @@ function Level() { return () => { editor.dispose() } }, []) - const uri = `file:///level${level}` + const uri = `file:///level${levelId}` // The next function will be called when the level changes useEffect(() => { connection.whenLeanClientStarted((leanClient) => { if (editor) { + const model = monaco.editor.createModel('', 'lean4', monaco.Uri.parse(uri)) editor.setModel(model) @@ -112,9 +121,10 @@ function Level() { new AbbreviationRewriter(new AbbreviationProvider(), model, editor) - leanClient.sendRequest("loadLevel", {world: "TestWorld", level}).then((res) => { + + leanClient.sendRequest("loadLevel", {world: "TestWorld", level: levelId}).then((res) => { // setLevelTitle("Level " + res["index"] + ": " + res["title"]) - setIndex(parseInt(res["index"])) + // setIndex(parseInt(res["index"])) setTacticDocs(res["tactics"]) setLemmaDocs(res["lemmas"]) setIntroduction(res["introduction"]) @@ -124,7 +134,8 @@ function Level() { return () => { model.dispose(); setReady(false) } } }) - }, [editor, level, connection]) + + }, [editor, levelId, connection]) function loadLevel(index) { setCompleted(false) @@ -148,8 +159,10 @@ function Level() { - - + + + +
diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx index 1ab8ef8..8dadaf5 100644 --- a/client/src/components/Welcome.tsx +++ b/client/src/components/Welcome.tsx @@ -11,6 +11,8 @@ import cytoscape from 'cytoscape' import klay from 'cytoscape-klay'; import { useSelector, useDispatch } from 'react-redux' import { fetchGame } from '../game/gameSlice' +import { Link as RouterLink } from 'react-router-dom'; + cytoscape.use( klay ); @@ -19,13 +21,8 @@ import { LeanClient } from 'lean4web/client/src/editor/leanclient'; import { ConnectionContext } from '../connection'; import { useAppDispatch, useAppSelector } from '../hooks'; -interface WelcomeProps { - setNbLevels: any; - startGame: any; - setConclusion: any; -} -function Welcome({ setNbLevels, startGame, setConclusion }: WelcomeProps) { +function Welcome() { const dispatch = useAppDispatch() const worldsRef = useRef(null) @@ -94,7 +91,7 @@ function Welcome({ setNbLevels, startGame, setConclusion }: WelcomeProps) { - +
diff --git a/client/src/index.tsx b/client/src/index.tsx index e65596d..1c0799d 100644 --- a/client/src/index.tsx +++ b/client/src/index.tsx @@ -2,7 +2,6 @@ import * as React from 'react'; import { createRoot } from 'react-dom/client'; import './index.css'; import App from './App'; -import Level from './components/Level'; import { ConnectionContext, connection } from './connection' import { store } from './store'; import { Provider } from 'react-redux'; @@ -11,18 +10,26 @@ import { RouterProvider, Route, } from "react-router-dom"; -import "./index.css"; +import ErrorPage from './ErrorPage'; +import Welcome from './components/Welcome'; +import Level from './components/Level'; import { monacoSetup } from 'lean4web/client/src/monacoSetup'; monacoSetup() + const router = createHashRouter([ { path: "/", element: , + errorElement: , children: [ { path: "/", + element: , + }, + { + path: "/level/:levelId", element: , }, ], diff --git a/package-lock.json b/package-lock.json index c53dec7..377ba69 100644 --- a/package-lock.json +++ b/package-lock.json @@ -14,6 +14,7 @@ "@mui/material": "^5.10.9", "@reduxjs/toolkit": "^1.9.0", "@types/cytoscape": "^3.19.9", + "@types/react-router-dom": "^5.3.3", "better-react-mathjax": "^2.0.2", "cytoscape": "^3.23.0", "cytoscape-klay": "^3.1.4", @@ -24,6 +25,7 @@ "react-dom": "^18.2.0", "react-markdown": "^8.0.3", "react-redux": "^8.0.5", + "react-router-dom": "^6.4.4", "vscode-ws-jsonrpc": "^2.0.0", "ws": "^8.9.0" }, @@ -2065,6 +2067,14 @@ } } }, + "node_modules/@remix-run/router": { + "version": "1.0.4", + "resolved": "https://registry.npmjs.org/@remix-run/router/-/router-1.0.4.tgz", + "integrity": "sha512-gTL8H5USTAKOyVA4xczzDJnC3HMssdFa3tRlwBicXynx9XfiXwneHnYQogwSKpdCkjXISrEKSTtX62rLpNEVQg==", + "engines": { + "node": ">=14" + } + }, "node_modules/@testing-library/dom": { "version": "8.19.0", "resolved": "https://registry.npmjs.org/@testing-library/dom/-/dom-8.19.0.tgz", @@ -2286,6 +2296,11 @@ "@types/unist": "*" } }, + "node_modules/@types/history": { + "version": "4.7.11", + "resolved": "https://registry.npmjs.org/@types/history/-/history-4.7.11.tgz", + "integrity": "sha512-qjDJRrmvBMiTx+jyLxvLfJU7UznFuokDv4f3WRuriHKERccVpFU+8XMQUAbDzoiJCsmexxRExQeMwwCdamSKDA==" + }, "node_modules/@types/hoist-non-react-statics": { "version": "3.3.1", "resolved": "https://registry.npmjs.org/@types/hoist-non-react-statics/-/hoist-non-react-statics-3.3.1.tgz", @@ -2386,6 +2401,25 @@ "@types/react": "*" } }, + "node_modules/@types/react-router": { + "version": "5.1.19", + "resolved": "https://registry.npmjs.org/@types/react-router/-/react-router-5.1.19.tgz", + "integrity": "sha512-Fv/5kb2STAEMT3wHzdKQK2z8xKq38EDIGVrutYLmQVVLe+4orDFquU52hQrULnEHinMKv9FSA6lf9+uNT1ITtA==", + "dependencies": { + "@types/history": "^4.7.11", + "@types/react": "*" + } + }, + "node_modules/@types/react-router-dom": { + "version": "5.3.3", + "resolved": "https://registry.npmjs.org/@types/react-router-dom/-/react-router-dom-5.3.3.tgz", + "integrity": "sha512-kpqnYK4wcdm5UaWI3fLcELopqLrHgLqNsdpHauzlQktfkHL3npOSwtj1Uz9oKBAzs7lFtVkV8j83voAz2D8fhw==", + "dependencies": { + "@types/history": "^4.7.11", + "@types/react": "*", + "@types/react-router": "*" + } + }, "node_modules/@types/react-transition-group": { "version": "4.4.5", "resolved": "https://registry.npmjs.org/@types/react-transition-group/-/react-transition-group-4.4.5.tgz", @@ -6816,6 +6850,36 @@ "node": ">=0.10.0" } }, + "node_modules/react-router": { + "version": "6.4.4", + "resolved": "https://registry.npmjs.org/react-router/-/react-router-6.4.4.tgz", + "integrity": "sha512-SA6tSrUCRfuLWeYsTJDuriRqfFIsrSvuH7SqAJHegx9ZgxadE119rU8oOX/rG5FYEthpdEaEljdjDlnBxvfr+Q==", + "dependencies": { + "@remix-run/router": "1.0.4" + }, + "engines": { + "node": ">=14" + }, + "peerDependencies": { + "react": ">=16.8" + } + }, + "node_modules/react-router-dom": { + "version": "6.4.4", + "resolved": "https://registry.npmjs.org/react-router-dom/-/react-router-dom-6.4.4.tgz", + "integrity": "sha512-0Axverhw5d+4SBhLqLpzPhNkmv7gahUwlUVIOrRLGJ4/uwt30JVajVJXqv2Qr/LCwyvHhQc7YyK1Do8a9Jj7qA==", + "dependencies": { + "@remix-run/router": "1.0.4", + "react-router": "6.4.4" + }, + "engines": { + "node": ">=14" + }, + "peerDependencies": { + "react": ">=16.8", + "react-dom": ">=16.8" + } + }, "node_modules/react-split": { "version": "2.0.14", "resolved": "https://registry.npmjs.org/react-split/-/react-split-2.0.14.tgz", @@ -10181,6 +10245,11 @@ "reselect": "^4.1.7" } }, + "@remix-run/router": { + "version": "1.0.4", + "resolved": "https://registry.npmjs.org/@remix-run/router/-/router-1.0.4.tgz", + "integrity": "sha512-gTL8H5USTAKOyVA4xczzDJnC3HMssdFa3tRlwBicXynx9XfiXwneHnYQogwSKpdCkjXISrEKSTtX62rLpNEVQg==" + }, "@testing-library/dom": { "version": "8.19.0", "resolved": "https://registry.npmjs.org/@testing-library/dom/-/dom-8.19.0.tgz", @@ -10373,6 +10442,11 @@ "@types/unist": "*" } }, + "@types/history": { + "version": "4.7.11", + "resolved": "https://registry.npmjs.org/@types/history/-/history-4.7.11.tgz", + "integrity": "sha512-qjDJRrmvBMiTx+jyLxvLfJU7UznFuokDv4f3WRuriHKERccVpFU+8XMQUAbDzoiJCsmexxRExQeMwwCdamSKDA==" + }, "@types/hoist-non-react-statics": { "version": "3.3.1", "resolved": "https://registry.npmjs.org/@types/hoist-non-react-statics/-/hoist-non-react-statics-3.3.1.tgz", @@ -10473,6 +10547,25 @@ "@types/react": "*" } }, + "@types/react-router": { + "version": "5.1.19", + "resolved": "https://registry.npmjs.org/@types/react-router/-/react-router-5.1.19.tgz", + "integrity": "sha512-Fv/5kb2STAEMT3wHzdKQK2z8xKq38EDIGVrutYLmQVVLe+4orDFquU52hQrULnEHinMKv9FSA6lf9+uNT1ITtA==", + "requires": { + "@types/history": "^4.7.11", + "@types/react": "*" + } + }, + "@types/react-router-dom": { + "version": "5.3.3", + "resolved": "https://registry.npmjs.org/@types/react-router-dom/-/react-router-dom-5.3.3.tgz", + "integrity": "sha512-kpqnYK4wcdm5UaWI3fLcELopqLrHgLqNsdpHauzlQktfkHL3npOSwtj1Uz9oKBAzs7lFtVkV8j83voAz2D8fhw==", + "requires": { + "@types/history": "^4.7.11", + "@types/react": "*", + "@types/react-router": "*" + } + }, "@types/react-transition-group": { "version": "4.4.5", "resolved": "https://registry.npmjs.org/@types/react-transition-group/-/react-transition-group-4.4.5.tgz", @@ -13687,6 +13780,23 @@ "integrity": "sha512-wViHqhAd8OHeLS/IRMJjTSDHF3U9eWi62F/MledQGPdJGDhodXJ9PBLNGr6WWL7qlH12Mt3TyTpbS+hGXMjCzQ==", "dev": true }, + "react-router": { + "version": "6.4.4", + "resolved": "https://registry.npmjs.org/react-router/-/react-router-6.4.4.tgz", + "integrity": "sha512-SA6tSrUCRfuLWeYsTJDuriRqfFIsrSvuH7SqAJHegx9ZgxadE119rU8oOX/rG5FYEthpdEaEljdjDlnBxvfr+Q==", + "requires": { + "@remix-run/router": "1.0.4" + } + }, + "react-router-dom": { + "version": "6.4.4", + "resolved": "https://registry.npmjs.org/react-router-dom/-/react-router-dom-6.4.4.tgz", + "integrity": "sha512-0Axverhw5d+4SBhLqLpzPhNkmv7gahUwlUVIOrRLGJ4/uwt30JVajVJXqv2Qr/LCwyvHhQc7YyK1Do8a9Jj7qA==", + "requires": { + "@remix-run/router": "1.0.4", + "react-router": "6.4.4" + } + }, "react-split": { "version": "2.0.14", "resolved": "https://registry.npmjs.org/react-split/-/react-split-2.0.14.tgz", diff --git a/package.json b/package.json index d1a64ec..b67aa8f 100644 --- a/package.json +++ b/package.json @@ -10,6 +10,7 @@ "@mui/material": "^5.10.9", "@reduxjs/toolkit": "^1.9.0", "@types/cytoscape": "^3.19.9", + "@types/react-router-dom": "^5.3.3", "better-react-mathjax": "^2.0.2", "cytoscape": "^3.23.0", "cytoscape-klay": "^3.1.4", @@ -20,6 +21,7 @@ "react-dom": "^18.2.0", "react-markdown": "^8.0.3", "react-redux": "^8.0.5", + "react-router-dom": "^6.4.4", "vscode-ws-jsonrpc": "^2.0.0", "ws": "^8.9.0" },