diff --git a/client/src/App.tsx b/client/src/App.tsx
index 7be4e5b..d43a626 100644
--- a/client/src/App.tsx
+++ b/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 =
- } else if (curLevel > 0) {
- mainComponent =
- } else {
- mainComponent =
- }
-
const title = useAppSelector(state => state.game.title)
return (
@@ -65,7 +56,7 @@ function App() {
- {mainComponent}
+
)
diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 6312d80..fc4c97e 100644
--- a/client/src/components/Level.tsx
+++ b/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,33 +101,35 @@ function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: Lev
// The next function will be called when the level changes
useEffect(() => {
- if (editor) {
- const model = monaco.editor.createModel('', 'lean4', monaco.Uri.parse(uri))
-
- editor.setModel(model)
- infoviewApi.serverRestarted(leanClient.initializeResult)
- infoProvider.openPreview(editor, infoviewApi)
- setReady(true)
-
- new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
-
- leanClient.sendRequest("loadLevel", {world: "TestWorld", level}).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) }
- }
- }, [editor, level, leanClient])
+ connection.whenLeanClientStarted((leanClient) => {
+ if (editor) {
+ const model = monaco.editor.createModel('', 'lean4', monaco.Uri.parse(uri))
+
+ editor.setModel(model)
+ infoviewApi.serverRestarted(leanClient.initializeResult)
+ infoProvider.openPreview(editor, infoviewApi)
+ setReady(true)
+
+ new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
+
+ leanClient.sendRequest("loadLevel", {world: "TestWorld", level}).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) }
+ }
+ })
+ }, [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
-
+
-
+
{ setExpertInfoview(!expertInfoview) }} control={} label="Expert mode" />
diff --git a/client/src/connection.ts b/client/src/connection.ts
index c212769..5382b49 100644
--- a/client/src/connection.ts
+++ b/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);
diff --git a/client/src/game/gameSlice.ts b/client/src/game/gameSlice.ts
index 9210755..798e2cb 100644
--- a/client/src/game/gameSlice.ts
+++ b/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))
})
})
diff --git a/client/src/index.tsx b/client/src/index.tsx
index 749feb9..e65596d 100644
--- a/client/src/index.tsx
+++ b/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: ,
+ children: [
+ {
+ path: "/",
+ element: ,
+ },
+ ],
+ },
+]);
const container = document.getElementById('root');
const root = createRoot(container!);
root.render(
-
-
+
+
diff --git a/client/src/store.ts b/client/src/store.ts
index 08c3899..ce09847 100644
--- a/client/src/store.ts
+++ b/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 }
}
})
});