load number of levels from server

client/src/components/Level.tsx

@@ -20,7 +20,7 @@ import './level.css'
 import { ConnectionContext } from '../connection';
 import Infoview from './Infoview';
 import { useParams } from 'react-router-dom';
-import { useLoadLevelQuery } from '../state/api';
+import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api';
 import { codeEdited, selectCode } from '../state/progress';
 import { useAppDispatch } from '../hooks';
 import { useSelector } from 'react-redux';
@@ -121,6 +121,8 @@ function Level() {
 
   const connection = React.useContext(ConnectionContext)
 
+  const gameInfo = useGetGameInfoQuery()
+
   const level = useLoadLevelQuery({world: worldId, level: levelId})
 
   const dispatch = useAppDispatch()
@@ -171,7 +173,7 @@ function Level() {
         <Grid xs={4} className="info-panel">
 
           <Button disabled={levelId <= 1} component={RouterLink} to={`/world/${worldId}/level/${levelId - 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Previous Level</Button>
-          <Button disabled={false} component={RouterLink} to={`/world/${worldId}/level/${levelId + 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Next Level</Button>
+          <Button disabled={levelId >= gameInfo.data?.worldSize[worldId]} component={RouterLink} to={`/world/${worldId}/level/${levelId + 1}`} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Next Level</Button>
 
           <div style={{display: expertInfoview ? 'block' : 'none' }} ref={infoviewRef} className="infoview vscode-light"></div>
           <div style={{display: expertInfoview ? 'none' : 'block' }}>

client/src/components/Welcome.tsx

@@ -30,6 +30,34 @@ function Welcome() {
 
   const padding = 10
 
+  const svgElements = []
+
+  if (gameInfo.data) {
+    for (let edge of gameInfo.data.worlds.edges) {
+      svgElements.push(
+        <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"/>
+      )
+    }
+    for (let id in nodes) {
+      let position: cytoscape.Position = nodes[id]
+
+      svgElements.push(
+        <Link to={`/world/${id}/level/1`}>
+          <circle fill="#61DAFB" cx={position.x} cy={position.y} r="8" />
+          <text style={{font: "italic 2px sans-serif",  "text-anchor": "middle", "dominant-baseline": "middle"} as any} x={position.x} y={position.y}>{id}</text>
+        </Link>
+      )
+
+      for (let i = 1; i <= gameInfo.data.worldSize[id]; i++) {
+        svgElements.push(
+          <Link to={`/world/${id}/level/${i}`}>
+            <circle fill="#aaa" cx={position.x + Math.sin(i/5) * 9} cy={position.y - Math.cos(i/5) * 9} r="0.8" />
+          </Link>
+        )
+      }
+    }
+  }
+
   return <div>
   { gameInfo.isLoading?
     <Box display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
@@ -43,13 +71,7 @@ function Welcome() {
       <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) =>
+          {svgElements}
-            <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>

client/src/state/api.ts

@@ -5,6 +5,7 @@ interface GameInfo {
   title: null|string,
   introduction: null|string,
   worlds: null|{nodes: string[], edges: string[][]},
+  worldSize: null|{[key: string]: number},
   authors: null|string[],
   conclusion: null|string,
 }

server/leanserver/GameServer/Game.lean

@@ -24,13 +24,16 @@ open Lsp
 open JsonRpc
 open IO
 
-def getGame (game : Name): GameServerM Game := do
+def getGame (game : Name): GameServerM Json := do
   let some game ← getGame? game
     | throwServerError "Game not found"
-  return game
+  let gameJson : Json := toJson game
+  -- Add world sizes to Json object
+  let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size))
+  let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)])
+  return gameJson
 
 /--
-
 Fields:
 - description: Lemma in mathematical language.
 - descriptionGoal: Lemma printed as Lean-Code.

server/testgame/TestGame.lean

@@ -63,8 +63,7 @@ aber eigenständig sein)
 
 ### Spieler-Führung
 
-- Keine Möglichkeit zurück zu gehen und nach dem letzten Level kann man trotzdem
+- Keine Möglichkeit zurück zu gehen
-\"Next Level\" klicken
 - Fehlermeldungen sind nicht besonders Benutzerfreundlich: Ganz unverständliche sammeln,
 damit wir diese später modifizieren können.
 - Kann man Taktiken blockieren?