From 83bbcd850e228e39e8ce795c5fd607753ceb715f Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 14 Dec 2022 12:22:46 +0100
Subject: [PATCH 1/3] use svg for overview

---
 client/src/components/Welcome.tsx | 105 +++++++++++++++---------------
 client/src/game/api.ts            |   2 +-
 2 files changed, 52 insertions(+), 55 deletions(-)

diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx
index 7966c56..33a5bad 100644
--- a/client/src/components/Welcome.tsx
+++ b/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';
 
@@ -15,70 +15,22 @@ cytoscape.use( klay );
 
 import { Box, Typography, Button, CircularProgress, Grid } from '@mui/material';
 import { useGetGameInfoQuery } from '../game/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(() => {
-    if (gameInfo.data?.worlds) { drawWorlds(gameInfo.data.worlds); }
-  }, [gameInfo.data?.worlds])
+  const { nodes, bounds }: any = gameInfo.data ? computeWorldLayout(gameInfo.data?.worlds) : {nodes: []}
 
   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>
@@ -94,7 +46,18 @@ function Welcome() {
       <Box textAlign='center' sx={{ m: 5 }}>
         <Button component={RouterLink} to="/world/Logic/level/1" variant="contained">Start rescue mission</Button>
       </Box>
-      <div ref={worldsRef} style={{"width": "100%","height": "50em"}} />
+      <Box textAlign='center' sx={{ m: 5 }}>
+        <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>
   }
 
@@ -102,3 +65,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 }
+}
diff --git a/client/src/game/api.ts b/client/src/game/api.ts
index 784cfd7..d4f1684 100644
--- a/client/src/game/api.ts
+++ b/client/src/game/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,
 }

From 4114cbc3044d57cb901854676c02fbf41f3643f2 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 14 Dec 2022 12:23:42 +0100
Subject: [PATCH 2/3] remove button

---
 client/src/components/Welcome.tsx | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx
index 33a5bad..330d520 100644
--- a/client/src/components/Welcome.tsx
+++ b/client/src/components/Welcome.tsx
@@ -43,9 +43,6 @@ function Welcome() {
           </MathJax>
         </Typography>
       </Box>
-      <Box textAlign='center' sx={{ m: 5 }}>
-        <Button component={RouterLink} to="/world/Logic/level/1" variant="contained">Start rescue mission</Button>
-      </Box>
       <Box textAlign='center' sx={{ m: 5 }}>
         <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}` : ''}>

From 32b9d028a7dfec6a9725ab3316342ade09056a6f Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 14 Dec 2022 14:02:57 +0100
Subject: [PATCH 3/3] save state of code

---
 client/src/components/Level.tsx   | 28 ++++++++++++++++++++++------
 client/src/components/Welcome.tsx |  2 +-
 client/src/hooks.ts               |  2 +-
 client/src/index.tsx              |  2 +-
 client/src/{game => state}/api.ts |  4 ++--
 client/src/state/progress.ts      | 30 ++++++++++++++++++++++++++++++
 client/src/{ => state}/store.ts   | 10 ++++++----
 7 files changed, 63 insertions(+), 15 deletions(-)
 rename client/src/{game => state}/api.ts (93%)
 create mode 100644 client/src/state/progress.ts
 rename client/src/{ => state}/store.ts (68%)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index fc4723f..9bbe71c 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -21,7 +21,10 @@ 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';
 
 
 
@@ -45,7 +48,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>
@@ -84,7 +97,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)
 
@@ -128,8 +141,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) ??
-          monaco.editor.createModel('', 'lean4', uri)
+        let model = monaco.editor.getModel(uri)
+        if (!model) {
+          model = monaco.editor.createModel(initialCode, 'lean4', uri)
+          model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
+        }
 
         editor.setModel(model)
         infoviewApi.serverRestarted(leanClient.initializeResult)
@@ -139,7 +155,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}
diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx
index 330d520..45b4063 100644
--- a/client/src/components/Welcome.tsx
+++ b/client/src/components/Welcome.tsx
@@ -14,7 +14,7 @@ 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';
 
 
diff --git a/client/src/hooks.ts b/client/src/hooks.ts
index 60a4163..afdce0a 100644
--- a/client/src/hooks.ts
+++ b/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
diff --git a/client/src/index.tsx b/client/src/index.tsx
index 9c9790b..f936b83 100644
--- a/client/src/index.tsx
+++ b/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,
diff --git a/client/src/game/api.ts b/client/src/state/api.ts
similarity index 93%
rename from client/src/game/api.ts
rename to client/src/state/api.ts
index d4f1684..5ee564a 100644
--- a/client/src/game/api.ts
+++ b/client/src/state/api.ts
@@ -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
diff --git a/client/src/state/progress.ts b/client/src/state/progress.ts
new file mode 100644
index 0000000..6e65467
--- /dev/null
+++ b/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
diff --git a/client/src/store.ts b/client/src/state/store.ts
similarity index 68%
rename from client/src/store.ts
rename to client/src/state/store.ts
index 1e6b216..927460e 100644
--- a/client/src/store.ts
+++ b/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