merge

client/src/components/Level.tsx

@@ -22,30 +22,22 @@ import './level.css'
 import { ConnectionContext } from '../connection';
 import Infoview from './Infoview';
 import { useParams } from 'react-router-dom';
-import { useLoadLevelQuery } from '../game/api';
+import { useLoadLevelQuery } from '../state/api';
+import { codeEdited, selectCode } from '../state/progress';
+import { useAppDispatch } from '../hooks';
+import { useSelector } from 'react-redux';
+
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faUpload, faArrowRotateRight, faChevronLeft, faChevronRight, faBook, faDownload } from '@fortawesome/free-solid-svg-icons'
 
 import { styled, useTheme, Theme, CSSObject } from '@mui/material/styles';
-import MuiAppBar, { AppBarProps as MuiAppBarProps } from '@mui/material/AppBar';
+import { AppBarProps as MuiAppBarProps } from '@mui/material/AppBar';
-import Toolbar from '@mui/material/Toolbar';
-import List from '@mui/material/List';
-import CssBaseline from '@mui/material/CssBaseline';
-import Typography from '@mui/material/Typography';
 import Divider from '@mui/material/Divider';
-import MenuIcon from '@mui/icons-material/Menu';
+
-import ChevronLeftIcon from '@mui/icons-material/ChevronLeft';
-import ChevronRightIcon from '@mui/icons-material/ChevronRight';
-import ListItem from '@mui/material/ListItem';
-import ListItemButton from '@mui/material/ListItemButton';
-import ListItemIcon from '@mui/material/ListItemIcon';
-import ListItemText from '@mui/material/ListItemText';
-import InboxIcon from '@mui/icons-material/MoveToInbox';
-import MailIcon from '@mui/icons-material/Mail';
 
 
 /** Drawer Test */
-const drawerWidth = 400;
+const drawerWidth = 400; /* TODO: This width is hard-coded. Fix me. */
 
 const openedMixin = (theme: Theme): CSSObject => ({
   width: drawerWidth,
@@ -130,7 +122,17 @@ function Level() {
   const connection = React.useContext(ConnectionContext)
 
   const level = useLoadLevelQuery({world: worldId, level: levelId})
-  const {editor, infoProvider} = useLevelEditor(worldId, levelId, codeviewRef, infoviewRef)
+
+  const dispatch = useAppDispatch()
+
+  const onDidChangeContent = (code) => {
+    dispatch(codeEdited({world: worldId, level: levelId, code}))
+  }
+
+  const initialCode = useSelector(selectCode(worldId, levelId))
+
+  const {editor, infoProvider} =
+    useLevelEditor(worldId, levelId, codeviewRef, infoviewRef, initialCode, onDidChangeContent)
 
   return <>
     <Box style={level.isLoading ? null : {display: "none"}} display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
@@ -177,7 +179,7 @@ function Level() {
 export default Level
 
 
-function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewRef) {
+function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewRef, initialCode, onDidChangeContent) {
 
   const connection = React.useContext(ConnectionContext)
 
@@ -221,8 +223,11 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewR
       if (editor) {
 
         const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`)
-        const model = monaco.editor.getModel(uri) ??
+        let model = monaco.editor.getModel(uri)
-          monaco.editor.createModel('', 'lean4', uri)
+        if (!model) {
+          model = monaco.editor.createModel(initialCode, 'lean4', uri)
+          model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
+        }
 
         editor.setModel(model)
         infoviewApi.serverRestarted(leanClient.initializeResult)
@@ -232,7 +237,7 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewR
         new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
       }
     })
-
+    // TODO: Properly close the file to stop send "keepAlive" calls to the server
   }, [editor, levelId, connection])
 
   return {editor, infoProvider}

client/src/components/Welcome.tsx

@@ -6,7 +6,7 @@ import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
-import cytoscape from 'cytoscape'
+import cytoscape, { LayoutOptions } from 'cytoscape'
 import klay from 'cytoscape-klay';
 import { Link as RouterLink, useNavigate } from 'react-router-dom';
 
@@ -14,71 +14,23 @@ import { Link as RouterLink, useNavigate } from 'react-router-dom';
 cytoscape.use( klay );
 
 import { Box, Typography, Button, CircularProgress, Grid } from '@mui/material';
-import { useGetGameInfoQuery } from '../game/api';
+import { useGetGameInfoQuery } from '../state/api';
+import { Link } from 'react-router-dom';
 
 
 function Welcome() {
   const navigate = useNavigate();
 
-  const worldsRef = useRef<HTMLDivElement>(null)
-
-  const drawWorlds = (worlds) => {
-    let elements = []
-    for (let node of worlds.nodes) {
-      elements.push({ data: { id: node } })
-    }
-    for (let edge of worlds.edges) {
-      elements.push({
-        data: {
-          id: edge[0] + " --edge-to--> " + edge[1],
-          source: edge[0],
-          target: edge[1]
-        }
-      })
-    }
-    const layout : any = {name: "klay", klay: {direction: "DOWN"}}
-    const cy = cytoscape({ container: worldsRef.current!, elements, layout,
-      style: [ // the stylesheet for the graph
-        {
-          selector: 'node',
-          style: {
-            'background-color': '#666',
-            'label': 'data(id)'
-          }
-        },
-
-        {
-          selector: 'edge',
-          style: {
-            'width': 3,
-            'line-color': '#ccc',
-            'target-arrow-color': '#ccc',
-            'target-arrow-shape': 'triangle',
-            'curve-style': 'bezier'
-          }
-        }
-      ],
-      userPanningEnabled: false,
-      userZoomingEnabled: false,
-      autoungrabify: true,
-      autounselectify: true,
-    })
-
-    cy.on('click', 'node', function(evt){
-      navigate(`/world/${this.id()}/level/1`);
-    });
-  }
-
   const gameInfo = useGetGameInfoQuery()
 
-  useEffect(() => {
+  const { nodes, bounds }: any = gameInfo.data ? computeWorldLayout(gameInfo.data?.worlds) : {nodes: []}
-    if (gameInfo.data?.worlds) { drawWorlds(gameInfo.data.worlds); }
-  }, [gameInfo.data?.worlds])
 
   useEffect(() => {
     if (gameInfo.data?.title) window.document.title = gameInfo.data.title
   }, [gameInfo.data?.title])
 
+  const padding = 10
+
   return <div>
   { gameInfo.isLoading?
     <Box display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
@@ -92,9 +44,17 @@ function Welcome() {
         </Typography>
       </Box>
       <Box textAlign='center' sx={{ m: 5 }}>
-        <Button component={RouterLink} to="/world/Logic/level/1" variant="contained">Start rescue mission</Button>
+        <svg xmlns="http://www.w3.org/2000/svg" xmlnsXlink="http://www.w3.org/1999/xlink" width="30%"
+            viewBox={bounds ? `${bounds.x1 - padding} ${bounds.y1 - padding} ${bounds.x2 - bounds.x1 + 2 * padding} ${bounds.y2 - bounds.y1 + 2 * padding}` : ''}>
+          {gameInfo.data ? gameInfo.data.worlds.edges.map((edge) =>
+            <line x1={nodes[edge[0]].x} y1={nodes[edge[0]].y} x2={nodes[edge[1]].x} y2={nodes[edge[1]].y} stroke="#1976d2" stroke-width="1"/>) : null}
+          {Object.entries(nodes).map(([id, position]) =>
+            <Link to={`/world/${id}/level/1`}>
+              <circle fill="#61DAFB" cx={(position as cytoscape.Position).x} cy={(position as cytoscape.Position).y} r="8" />
+              <text style={{font: "italic 2px sans-serif",  "text-anchor": "middle", "dominant-baseline": "middle"} as any} x={(position as cytoscape.Position).x} y={(position as cytoscape.Position).y}>{id}</text>
+            </Link>)}
+        </svg>
       </Box>
-      <div ref={worldsRef} style={{"width": "100%","height": "50em"}} />
     </div>
   }
 
@@ -102,3 +62,37 @@ function Welcome() {
 }
 
 export default Welcome
+
+function computeWorldLayout(worlds) {
+
+  let elements = []
+  for (let node of worlds.nodes) {
+    elements.push({ data: { id: node } })
+  }
+  for (let edge of worlds.edges) {
+    elements.push({
+      data: {
+        id: edge[0] + " --edge-to--> " + edge[1],
+        source: edge[0],
+        target: edge[1]
+      }
+    })
+  }
+
+  const cy = cytoscape({
+    container: null,
+    elements,
+    headless: true,
+    styleEnabled: false
+  })
+
+  const layout = cy.layout({name: "klay", klay: {direction: "DOWN"}} as LayoutOptions).run()
+  let nodes = {}
+  cy.nodes().forEach((node, id) => {
+    nodes[node.id()] = node.position()
+    console.log(node.position())
+  })
+  const bounds = cy.nodes().boundingBox()
+  console.log(bounds)
+  return { nodes, bounds }
+}

client/src/hooks.ts

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

client/src/index.tsx

@@ -3,7 +3,7 @@ import { createRoot } from 'react-dom/client';
 import './index.css';
 import App from './App';
 import { ConnectionContext, connection } from './connection'
-import { store } from './store';
+import { store } from './state/store';
 import { Provider } from 'react-redux';
 import {
   createHashRouter,

client/src/state/api.ts

@@ -4,7 +4,7 @@ import { Connection } from '../connection'
 interface GameInfo {
   title: null|string,
   introduction: null|string,
-  worlds: null|{nodes: string[], edges: string[][2]},
+  worlds: null|{nodes: string[], edges: string[][]},
   authors: null|string[],
   conclusion: null|string,
 }
@@ -37,7 +37,7 @@ const customBaseQuery = async (
 }
 
 // Define a service using a base URL and expected endpoints
-export const gameApi = createApi({
+export const apiSlice = createApi({
   reducerPath: 'gameApi',
   baseQuery: customBaseQuery,
   endpoints: (builder) => ({
@@ -52,4 +52,4 @@ export const gameApi = createApi({
 
 // Export hooks for usage in functional components, which are
 // auto-generated based on the defined endpoints
-export const { useGetGameInfoQuery, useLoadLevelQuery } = gameApi
+export const { useGetGameInfoQuery, useLoadLevelQuery } = apiSlice

client/src/state/progress.ts

@@ -0,0 +1,30 @@
+import { createSlice } from '@reduxjs/toolkit'
+import type { PayloadAction } from '@reduxjs/toolkit'
+
+interface ProgressState {
+  code: {[world: string]: {[level: number]: string}}
+}
+
+const initialState = { code: {} } as ProgressState
+
+export const progressSlice = createSlice({
+  name: 'progress',
+  initialState,
+  reducers: {
+    codeEdited(state, action: PayloadAction<{world: string, level: number, code: string}>) {
+      if (!state.code[action.payload.world]) {
+        state.code[action.payload.world] = {}
+      }
+      state.code[action.payload.world][action.payload.level] = action.payload.code
+    },
+  }
+})
+
+export function selectCode(world: string, level: number) {
+  return (state) => {
+    if (!state.progress.code[world]) { return undefined }
+    state.progress.code[world][level];
+  }
+}
+
+export const { codeEdited } = progressSlice.actions

client/src/state/store.ts

@@ -1,19 +1,21 @@
 import { configureStore } from '@reduxjs/toolkit';
-import { connection } from './connection'
+import { connection } from '../connection'
 import thunkMiddleware from 'redux-thunk'
-import { gameApi } from './game/api'
+import { apiSlice } from './api'
+import { progressSlice } from './progress'
 
 
 export const store = configureStore({
   reducer: {
-    [gameApi.reducerPath]: gameApi.reducer,
+    [apiSlice.reducerPath]: apiSlice.reducer,
+    [progressSlice.name]: progressSlice.reducer,
   },
   middleware: getDefaultMiddleware =>
     getDefaultMiddleware({
       thunk: {
         extraArgument: { connection }
       }
-    }).concat(gameApi.middleware),
+    }).concat(apiSlice.middleware),
 });
 
 // Infer the `RootState` and `AppDispatch` types from the store itself