routing for level

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() {

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 (
+    <div id="error-page">
+      <h1>Oops!</h1>
+      <p>Sorry, an unexpected error has occurred.</p>
+      <p>
+        <i>{error.statusText || error.message}</i>
+      </p>
+    </div>
+  );
+}

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<monaco.editor.IStandaloneCodeEditor|null>(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() {
         </div>
       </Grid>
       <Grid xs={4} className="info-panel">
-        <Button disabled={index <= 1} onClick={() => { loadLevel(index - 1) }} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Previous Level</Button>
+
-        <Button disabled={index >= 99} onClick={() => { loadLevel(index + 1) }} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Next Level</Button>
+        <Button disabled={levelId <= 1} component={RouterLink} to={`/level/${levelId - 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Previous Level</Button>
+        <Button disabled={false} component={RouterLink} to={`/level/${levelId + 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Next Level</Button>
+
         <div style={{display: expertInfoview ? 'block' : 'none' }} ref={infoviewRef} className="infoview vscode-light"></div>
         <div style={{display: expertInfoview ? 'none' : 'block' }}>
           <Infoview leanClient={connection.getLeanClient()} editor={editor} editorApi={infoProvider?.getApi()} />

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<HTMLDivElement>(null)
@@ -94,7 +91,7 @@ function Welcome({ setNbLevels, startGame, setConclusion }: WelcomeProps) {
         </Typography>
       </Box>
       <Box textAlign='center' sx={{ m: 5 }}>
-        <Button onClick={startGame} variant="contained">Start rescue mission</Button>
+        <Button component={RouterLink} to="/level/1" variant="contained">Start rescue mission</Button>
       </Box>
       <div ref={worldsRef} style={{"width": "100%","height": "50em"}} />
     </div>

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: <App />,
+    errorElement: <ErrorPage />,
     children: [
       {
         path: "/",
+        element: <Welcome />,
+      },
+      {
+        path: "/level/:levelId",
         element: <Level />,
       },
     ],

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",

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"
   },