use react router, reorganize leanClient connection

client/src/App.tsx

@@ -3,6 +3,7 @@ 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';
 import '@fontsource/roboto/400.css';
@@ -14,7 +15,6 @@ import { AppBar, CssBaseline, Toolbar, Typography } from '@mui/material';
 import Welcome from './components/Welcome';
 import Level from './components/Level';
 import GoodBye from './components/GoodBye';
-import { monacoSetup } from 'lean4web/client/src/monacoSetup'
 import { useAppSelector } from './hooks';
 
 function App() {
@@ -40,15 +40,6 @@ function App() {
     setCurLevel(1)
   }
 
-  let mainComponent;
-  if (finished) {
-    mainComponent = <GoodBye message={conclusion} />
-  } else if (curLevel > 0) {
-    mainComponent = <Level nbLevels={99} level={curLevel} setCurLevel={setCurLevel} setLevelTitle={setLevelTitle} setFinished={setFinished}/>
-  } else {
-    mainComponent = <Welcome setNbLevels={setNbLevels} startGame={startGame} setConclusion={setConclusion}/>
-  }
-
   const title = useAppSelector(state => state.game.title)
 
   return (
@@ -65,7 +56,7 @@ function App() {
         </Typography>
         </Toolbar>
       </AppBar>
-      {mainComponent}
+      <Outlet />
     </MathJaxContext>
     </div>
   )

client/src/components/Level.tsx

@@ -11,10 +11,6 @@ import { Button, FormControlLabel, FormGroup, Switch } from '@mui/material';
 import Grid from '@mui/material/Unstable_Grid2';
 
 import LeftPanel from './LeftPanel';
-import InputZone from './InputZone';
-import Message from './Message';
-import TacticState from './TacticState';
-import { LeanClient } from 'lean4web/client/src/editor/leanclient';
 import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
 import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
 import { InfoProvider } from 'lean4web/client/src/editor/infoview';
@@ -25,15 +21,8 @@ import './level.css'
 import { ConnectionContext } from '../connection';
 import Infoview from './Infoview';
 
-interface LevelProps {
-  nbLevels: any;
-  level: any;
-  setCurLevel: any;
-  setLevelTitle: any;
-  setFinished: any
-}
-
-function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: LevelProps) {
+function Level() {
+  const level = 1
   const [index, setIndex] = useState(level) // Level number
   const [tacticDocs, setTacticDocs] = useState([])
   const [lemmaDocs, setLemmaDocs] = useState([])
@@ -77,7 +66,7 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
     messagePanelRef.current!.scrollTo(0,0)
   }, [level])
 
-  const leanClient = React.useContext(ConnectionContext)
+  const connection = React.useContext(ConnectionContext)
 
   useEffect(() => {
     const editor = monaco.editor.create(codeviewRef.current!, {
@@ -97,7 +86,7 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
       theme: 'vs-code-theme-converted'
     })
 
-    const infoProvider = new InfoProvider(leanClient)
+    const infoProvider = new InfoProvider(connection.getLeanClient())
     const div: HTMLElement = infoviewRef.current!
     const infoviewApi = renderInfoview(infoProvider.getApi(), div)
 
@@ -112,6 +101,7 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
 
   // 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))
 
@@ -123,7 +113,7 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
         new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
 
         leanClient.sendRequest("loadLevel", {world: "TestWorld", level}).then((res) => {
-        setLevelTitle("Level " + res["index"] + ": " + res["title"])
+          // setLevelTitle("Level " + res["index"] + ": " + res["title"])
           setIndex(parseInt(res["index"]))
           setTacticDocs(res["tactics"])
           setLemmaDocs(res["lemmas"])
@@ -133,12 +123,13 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
 
         return () => { model.dispose(); setReady(false) }
       }
-  }, [editor, level, leanClient])
+    })
+  }, [editor, level, connection])
 
   function loadLevel(index) {
     setCompleted(false)
     setHistory([])
-    setCurLevel(index)
+    // setCurLevel(index)
   }
 
   return (
@@ -158,10 +149,10 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
       </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 >= nbLevels} onClick={() => { loadLevel(index + 1) }} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Next Level</Button>
+        <Button disabled={index >= 99} onClick={() => { loadLevel(index + 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={leanClient} editor={editor} editorApi={infoProvider?.getApi()} />
+          <Infoview leanClient={connection.getLeanClient()} editor={editor} editorApi={infoProvider?.getApi()} />
         </div>
         <FormGroup>
           <FormControlLabel onChange={() => { setExpertInfoview(!expertInfoview) }} control={<Switch />} label="Expert mode" />

client/src/connection.ts

@@ -1,15 +1,37 @@
 
-
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { LeanClient } from 'lean4web/client/src/editor/leanclient';
 import * as React from 'react';
-import { monacoSetup } from 'lean4web/client/src/monacoSetup';
 
-monacoSetup()
 
-const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/'
+export class Connection {
+  private leanClient = null
+
+  getLeanClient() {
+    if (this.leanClient === null) {
+      const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/'
+
+      const uri = monaco.Uri.parse('file:///')
+      this.leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
+    }
+
+    return this.leanClient
+  }
+
+  /** Call `callback` when the leanClient has started. If not already started, start it. */
+  whenLeanClientStarted = (callback) => {
+    const leanClient = this.getLeanClient()
+    if (leanClient.isRunning()) {
+      callback(leanClient)
+    } else {
+      if (!leanClient.isStarted()) {
+        leanClient.start()
+      }
+     leanClient.restarted(() => { callback(leanClient) })
+    }
+  }
+}
 
-const uri = monaco.Uri.parse('file:///')
-export const leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
+export const connection = new Connection()
 
 export const ConnectionContext = React.createContext(null);

client/src/game/gameSlice.ts

@@ -1,5 +1,6 @@
 import { createSlice, PayloadAction } from '@reduxjs/toolkit'
 import { LeanClient } from 'lean4web/client/src/editor/leanclient'
+import { Connection } from '../connection'
 import type { RootState } from '../store'
 
 interface GameState {
@@ -34,23 +35,11 @@ export const gameSlice = createSlice({
 
 export const { loadedGame } = gameSlice.actions
 
-// TODO: Move this into LeanClient?
-/** Call `callback` when the leanClient has started. If not already started, start it. */
-const whenLeanClientStarted = (leanClient, callback) => {
-  if (leanClient.isRunning()) {
-    callback()
-  } else {
-    if (!leanClient.isStarted()) {
-      leanClient.start()
-    }
-    leanClient.restarted(callback)
-  }
-}
 
 export const fetchGame = (dispatch, getState, extraArgument) => {
-  const leanClient : LeanClient = extraArgument.leanClient
-  whenLeanClientStarted(leanClient, () => {
-    leanClient.sendRequest("info", {}).then((res) =>{
+  const connection : Connection = extraArgument.connection
+  connection.whenLeanClientStarted(() => {
+    connection.getLeanClient().sendRequest("info", {}).then((res) =>{
       dispatch(loadedGame(res))
     })
   })

client/src/index.tsx

@@ -2,18 +2,40 @@ 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';
-import { ConnectionContext, leanClient } from './connection'
+import {
+  createHashRouter,
+  RouterProvider,
+  Route,
+} from "react-router-dom";
+import "./index.css";
+import { monacoSetup } from 'lean4web/client/src/monacoSetup';
 
+monacoSetup()
+
+const router = createHashRouter([
+  {
+    path: "/",
+    element: <App />,
+    children: [
+      {
+        path: "/",
+        element: <Level />,
+      },
+    ],
+  },
+]);
 
 const container = document.getElementById('root');
 const root = createRoot(container!);
 root.render(
   <React.StrictMode>
     <Provider store={store}>
-      <ConnectionContext.Provider value={leanClient}>
-        <App />
+      <ConnectionContext.Provider value={connection}>
+        <RouterProvider router={router} />
       </ConnectionContext.Provider>
     </Provider>
   </React.StrictMode>

client/src/store.ts

@@ -1,10 +1,10 @@
 import { configureStore } from '@reduxjs/toolkit';
 import gameReducer from './game/gameSlice';
-import { leanClient } from './connection'
+import { connection } from './connection'
 import thunkMiddleware from 'redux-thunk'
 
 
-const thunkMiddlewareWithArg = thunkMiddleware.withExtraArgument({ leanClient })
+const thunkMiddlewareWithArg = thunkMiddleware.withExtraArgument({ connection })
 
 export const store = configureStore({
   reducer: {
@@ -13,7 +13,7 @@ export const store = configureStore({
   middleware: getDefaultMiddleware =>
     getDefaultMiddleware({
       thunk: {
-        extraArgument: { leanClient }
+        extraArgument: { connection }
       }
     })
 });