use redux

client/src/App.tsx

@@ -14,29 +14,15 @@ import { AppBar, CssBaseline, Toolbar, Typography } from '@mui/material';
 import Welcome from './components/Welcome';
 import Level from './components/Level';
 import GoodBye from './components/GoodBye';
-import useWebSocket from 'react-use-websocket';
-import { LeanClient } from 'lean4web/client/src/editor/leanclient';
 import { monacoSetup } from 'lean4web/client/src/monacoSetup'
-
-const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/'
-
-monacoSetup()
+import { useAppSelector } from './hooks';
 
 function App() {
-  const [title, setTitle] = useState("")
   const [conclusion, setConclusion] = useState("")
   const [levelTitle, setLevelTitle] = useState("")
   const [nbLevels, setNbLevels] = useState(0)
   const [curLevel, setCurLevel] = useState(0)
   const [finished, setFinished] = useState(false)
-  const [leanClient, setLeanClient] = useState<null|LeanClient>(null)
-
-  useEffect(() => {
-    const uri = monaco.Uri.parse('file:///')
-    const leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
-    setLeanClient(leanClient)
-  }, [])
-
 
   const mathJaxConfig = {
     loader: {
@@ -58,11 +44,13 @@ function App() {
   if (finished) {
     mainComponent = <GoodBye message={conclusion} />
   } else if (curLevel > 0) {
-    mainComponent = <Level leanClient={leanClient} nbLevels={nbLevels} level={curLevel} setCurLevel={setCurLevel} setLevelTitle={setLevelTitle} setFinished={setFinished}/>
+    mainComponent = <Level nbLevels={nbLevels} level={curLevel} setCurLevel={setCurLevel} setLevelTitle={setLevelTitle} setFinished={setFinished}/>
   } else {
-    mainComponent = <Welcome leanClient={leanClient} setNbLevels={setNbLevels} setTitle={setTitle} startGame={startGame} setConclusion={setConclusion}/>
+    mainComponent = <Welcome setNbLevels={setNbLevels} startGame={startGame} setConclusion={setConclusion}/>
   }
 
+  const title = useAppSelector(state => state.game.title)
+
   return (
     <div className="App">
     <MathJaxContext config={mathJaxConfig}>

client/src/components/Level.tsx

@@ -22,9 +22,9 @@ import 'lean4web/client/src/editor/infoview.css'
 import { renderInfoview } from '@leanprover/infoview'
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import './level.css'
+import { ConnectionContext } from '../connection';
 
 interface LevelProps {
-  leanClient: null|LeanClient;
   nbLevels: any;
   level: any;
   setCurLevel: any;
@@ -32,7 +32,7 @@ interface LevelProps {
   setFinished: any
 }
 
-function Level({ leanClient, nbLevels, level, setCurLevel, setLevelTitle, setFinished }: LevelProps) {
+function Level({ nbLevels, level, setCurLevel, setLevelTitle, setFinished }: LevelProps) {
   const [index, setIndex] = useState(level) // Level number
   const [tacticDocs, setTacticDocs] = useState([])
   const [lemmaDocs, setLemmaDocs] = useState([])
@@ -72,6 +72,8 @@ function Level({ leanClient, nbLevels, level, setCurLevel, setLevelTitle, setFin
     messagePanelRef.current!.scrollTo(0,0)
   }, [level])
 
+  const leanClient = React.useContext(ConnectionContext)
+
   useEffect(() => {
     const editor = monaco.editor.create(codeviewRef.current!, {
       glyphMargin: true,

client/src/components/Welcome.tsx

@@ -9,30 +9,25 @@ import '@fontsource/roboto/700.css';
 import * as rpc from 'vscode-ws-jsonrpc';
 import cytoscape from 'cytoscape'
 import klay from 'cytoscape-klay';
+import { useSelector, useDispatch } from 'react-redux'
+import { fetchGame } from '../game/gameSlice'
 
 cytoscape.use( klay );
 
 import { Box, Typography, Button, CircularProgress, Grid } from '@mui/material';
 import { LeanClient } from 'lean4web/client/src/editor/leanclient';
+import { ConnectionContext } from '../connection';
+import { useAppDispatch, useAppSelector } from '../hooks';
 
 interface WelcomeProps {
-  leanClient: null|LeanClient;
   setNbLevels: any;
-  setTitle: any;
   startGame: any;
   setConclusion: any;
 }
 
-type infoResultType = {
-  title: string,
-  nb_levels: any[],
-  conclusion: string
-  worlds: {edges: string[][], nodes: string[]}
-}
+function Welcome({ setNbLevels, startGame, setConclusion }: WelcomeProps) {
+  const dispatch = useAppDispatch()
 
-function Welcome({ leanClient, setNbLevels, setTitle, startGame, setConclusion }: WelcomeProps) {
-
-  const [leanData, setLeanData] = useState<null|infoResultType>(null)
   const worldsRef = useRef<HTMLDivElement>(null)
 
   const drawWorlds = (worlds) => {
@@ -78,42 +73,34 @@ function Welcome({ leanClient, setNbLevels, setTitle, startGame, setConclusion }
     })
   }
 
-  useEffect(() => {
-    if (!leanClient) return;
+  useEffect(() => { dispatch(fetchGame); }, [])
 
-    const getInfo = async () => {
-      await leanClient.start() // TODO: need a way to wait for start without restarting
-      leanClient.sendRequest("info", {}).then((res: infoResultType) =>{
-        console.log(res)
-        setLeanData(res)
-        setNbLevels(res.nb_levels)
-        setTitle(res.title)
-        document.title = res.title
-        setConclusion(res.conclusion)
-        drawWorlds(res.worlds)
-      });
-    }
-    getInfo()
-  }, [leanClient])
+  const worlds = useAppSelector(state => state.game.worlds)
+  useEffect(() => { if (worlds) { drawWorlds(worlds); } }, [worlds])
 
-  let content
-  if (leanData) {
-    content = (<Box sx={{ m: 3 }}>
-      <Typography variant="body1" component="div">
-        <MathJax>
-          <ReactMarkdown>{leanData["introduction"]}</ReactMarkdown>
-        </MathJax>
-      </Typography>
+  const title = useAppSelector(state => state.game.title)
+  useEffect(() => { window.document.title = title }, [title])
+
+  const introduction = useAppSelector(state => state.game.introduction)
+
+  return <div>
+  { introduction?// TODO: find a better way to mark loading state?
+    <div>
+      <Box sx={{ m: 3 }}>
+        <Typography variant="body1" component="div">
+          <MathJax>
+            <ReactMarkdown>{introduction}</ReactMarkdown>
+          </MathJax>
+        </Typography>
+      </Box>
       <Box textAlign='center' sx={{ m: 5 }}>
         <Button onClick={startGame} variant="contained">Start rescue mission</Button>
       </Box>
-    </Box>)
-  } else {
-    content = <Box display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
+      <div ref={worldsRef} style={{"width": "100%","height": "50em"}} />
+    </div>
+    : <Box display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
   }
-  return <div>
-    <div>{content}</div>
-    <div ref={worldsRef} style={{"width": "100%","height": "50em"}} />
+
   </div>
 }
 

client/src/connection.ts

@@ -0,0 +1,15 @@
+
+
+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/'
+
+const uri = monaco.Uri.parse('file:///')
+export const leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
+
+export const ConnectionContext = React.createContext(null);

client/src/game/gameSlice.ts

@@ -0,0 +1,59 @@
+import { createSlice, PayloadAction } from '@reduxjs/toolkit'
+import { LeanClient } from 'lean4web/client/src/editor/leanclient'
+import type { RootState } from '../store'
+
+interface GameState {
+  title: null|string,
+  introduction: null|string,
+  worlds: null|{nodes: string[], edges: string[][2]},
+  authors: null|string[],
+  conclusion: null|string,
+}
+
+const initialState : GameState = {
+  title: null,
+  introduction: null,
+  worlds: null,
+  authors: null,
+  conclusion: null,
+}
+
+export const gameSlice = createSlice({
+  name: 'game',
+  initialState,
+  reducers: {
+    loadedGame: (state, action: PayloadAction<any>) => {
+      state.title = action.payload.title
+      state.introduction = action.payload.introduction
+      state.worlds = action.payload.worlds
+      state.authors = action.payload.authors
+      state.conclusion = action.payload.conclusion
+    },
+  },
+})
+
+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) =>{
+      dispatch(loadedGame(res))
+    })
+  })
+}
+
+export default gameSlice.reducer

client/src/hooks.ts

@@ -0,0 +1,6 @@
+import { TypedUseSelectorHook, useDispatch, useSelector } from 'react-redux'
+import type { RootState, AppDispatch } from './store'
+
+// Use throughout your app instead of plain `useDispatch` and `useSelector`
+export const useAppDispatch: () => AppDispatch = useDispatch
+export const useAppSelector: TypedUseSelectorHook<RootState> = useSelector

client/src/index.tsx

@@ -2,7 +2,19 @@ import * as React from 'react';
 import { createRoot } from 'react-dom/client';
 import './index.css';
 import App from './App';
+import { store } from './store';
+import { Provider } from 'react-redux';
+import { ConnectionContext, leanClient } from './connection'
+
 
 const container = document.getElementById('root');
 const root = createRoot(container!);
-root.render(<App />);
+root.render(
+  <React.StrictMode>
+    <Provider store={store}>
+      <ConnectionContext.Provider value={leanClient}>
+        <App />
+      </ConnectionContext.Provider>
+    </Provider>
+  </React.StrictMode>
+);

client/src/store.ts

@@ -0,0 +1,24 @@
+import { configureStore } from '@reduxjs/toolkit';
+import gameReducer from './game/gameSlice';
+import { leanClient } from './connection'
+import thunkMiddleware from 'redux-thunk'
+
+
+const thunkMiddlewareWithArg = thunkMiddleware.withExtraArgument({ leanClient })
+
+export const store = configureStore({
+  reducer: {
+    game: gameReducer,
+  },
+  middleware: getDefaultMiddleware =>
+    getDefaultMiddleware({
+      thunk: {
+        extraArgument: { leanClient }
+      }
+    })
+});
+
+// Infer the `RootState` and `AppDispatch` types from the store itself
+export type RootState = ReturnType<typeof store.getState>
+// Inferred type: {posts: PostsState, comments: CommentsState, users: UsersState}
+export type AppDispatch = typeof store.dispatch