From c6d8b358068b75f227f450c30c79f29c1573d1ec Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Fri, 9 Dec 2022 17:20:03 +0100 Subject: [PATCH] set up rtk query --- client/src/App.tsx | 2 +- client/src/components/Level.tsx | 2 +- client/src/components/Welcome.tsx | 29 ++++++++----------- client/src/connection.ts | 24 +++++++++------- client/src/game/api.ts | 38 ++++++++++++++++++++++++ client/src/game/gameSlice.ts | 48 ------------------------------- client/src/store.ts | 8 ++---- 7 files changed, 69 insertions(+), 82 deletions(-) create mode 100644 client/src/game/api.ts delete mode 100644 client/src/game/gameSlice.ts 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