diff --git a/client/src/App.tsx b/client/src/App.tsx
index 67cfc92..4ed7abd 100644
--- a/client/src/App.tsx
+++ b/client/src/App.tsx
@@ -35,7 +35,7 @@ function App() {
setCurLevel(1)
}
- const title = useAppSelector(state => state.game.title)
+ const title = ""//useAppSelector(state => state.gameApi.data.title)
return (
diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 0e00f68..e094771 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -110,7 +110,7 @@ function Level() {
// The next function will be called when the level changes
useEffect(() => {
- connection.whenLeanClientStarted((leanClient) => {
+ connection.startLeanClient().then((leanClient) => {
if (editor) {
const model = monaco.editor.createModel('', 'lean4', monaco.Uri.parse(uri))
diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx
index b032375..fe9f79c 100644
--- a/client/src/components/Welcome.tsx
+++ b/client/src/components/Welcome.tsx
@@ -6,24 +6,18 @@ import '@fontsource/roboto/300.css';
import '@fontsource/roboto/400.css';
import '@fontsource/roboto/500.css';
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'
import { Link as RouterLink, useNavigate } from 'react-router-dom';
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';
+import { useGetGameInfoQuery } from '../game/api';
function Welcome() {
- const dispatch = useAppDispatch()
const navigate = useNavigate();
const worldsRef = useRef
(null)
@@ -75,23 +69,25 @@ function Welcome() {
});
}
- useEffect(() => { dispatch(fetchGame); }, [])
+ const gameInfo = useGetGameInfoQuery()
- const worlds = useAppSelector(state => state.game.worlds)
- useEffect(() => { if (worlds) { drawWorlds(worlds); } }, [worlds])
+ useEffect(() => {
+ if (gameInfo.data?.worlds) { drawWorlds(gameInfo.data.worlds); }
+ }, [gameInfo.data?.worlds])
- const title = useAppSelector(state => state.game.title)
- useEffect(() => { window.document.title = title }, [title])
-
- const introduction = useAppSelector(state => state.game.introduction)
+ useEffect(() => {
+ if (gameInfo.data?.title) window.document.title = gameInfo.data.title
+ }, [gameInfo.data?.title])
return
- { introduction?// TODO: find a better way to mark loading state?
+ { gameInfo.isLoading?
+
+ :
- {introduction}
+ {gameInfo.data.introduction}
@@ -100,7 +96,6 @@ function Welcome() {
- :
}
diff --git a/client/src/connection.ts b/client/src/connection.ts
index 5382b49..73c96b5 100644
--- a/client/src/connection.ts
+++ b/client/src/connection.ts
@@ -18,17 +18,21 @@ export class Connection {
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()
+ /** If not already started, starts the Lean client. resolves the returned promise as soon as a
+ * Lean client is running.
+ */
+ startLeanClient = () => {
+ return new Promise((resolve) => {
+ const leanClient = this.getLeanClient()
+ if (leanClient.isRunning()) {
+ resolve(leanClient)
+ } else {
+ if (!leanClient.isStarted()) {
+ leanClient.start()
+ }
+ leanClient.restarted(() => { resolve(leanClient) })
}
- leanClient.restarted(() => { callback(leanClient) })
- }
+ })
}
}
diff --git a/client/src/game/api.ts b/client/src/game/api.ts
new file mode 100644
index 0000000..c23e18e
--- /dev/null
+++ b/client/src/game/api.ts
@@ -0,0 +1,38 @@
+import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react'
+import { Connection } from '../connection'
+
+interface GameState {
+ title: null|string,
+ introduction: null|string,
+ worlds: null|{nodes: string[], edges: string[][2]},
+ authors: null|string[],
+ conclusion: null|string,
+}
+
+const customBaseQuery = async (
+ args : {method: string, params?: any},
+ { signal, dispatch, getState, extra },
+ extraOptions
+) => {
+ const connection : Connection = extra.connection
+ let leanClient = await connection.startLeanClient()
+ console.log(`Sending request ${args.method}`)
+ let res = await leanClient.sendRequest(args.method, args.params)
+ console.log('Received response', res)
+ return {'data': res}
+}
+
+// Define a service using a base URL and expected endpoints
+export const gameApi = createApi({
+ reducerPath: 'gameApi',
+ baseQuery: customBaseQuery,
+ endpoints: (builder) => ({
+ getGameInfo: builder.query({
+ query: () => {return {method: 'info', params: {}}},
+ }),
+ }),
+})
+
+// Export hooks for usage in functional components, which are
+// auto-generated based on the defined endpoints
+export const { useGetGameInfoQuery } = gameApi
diff --git a/client/src/game/gameSlice.ts b/client/src/game/gameSlice.ts
deleted file mode 100644
index 798e2cb..0000000
--- a/client/src/game/gameSlice.ts
+++ /dev/null
@@ -1,48 +0,0 @@
-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 {
- 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) => {
- 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
-
-
-export const fetchGame = (dispatch, getState, extraArgument) => {
- const connection : Connection = extraArgument.connection
- connection.whenLeanClientStarted(() => {
- connection.getLeanClient().sendRequest("info", {}).then((res) =>{
- dispatch(loadedGame(res))
- })
- })
-}
-
-export default gameSlice.reducer
diff --git a/client/src/store.ts b/client/src/store.ts
index ce09847..1e6b216 100644
--- a/client/src/store.ts
+++ b/client/src/store.ts
@@ -1,21 +1,19 @@
import { configureStore } from '@reduxjs/toolkit';
-import gameReducer from './game/gameSlice';
import { connection } from './connection'
import thunkMiddleware from 'redux-thunk'
+import { gameApi } from './game/api'
-const thunkMiddlewareWithArg = thunkMiddleware.withExtraArgument({ connection })
-
export const store = configureStore({
reducer: {
- game: gameReducer,
+ [gameApi.reducerPath]: gameApi.reducer,
},
middleware: getDefaultMiddleware =>
getDefaultMiddleware({
thunk: {
extraArgument: { connection }
}
- })
+ }).concat(gameApi.middleware),
});
// Infer the `RootState` and `AppDispatch` types from the store itself