merge

client/src/components/Infoview.tsx

@@ -25,7 +25,7 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
   const [globalDiagnostics, setGlobalDiagnostics] = useState<any[]>(undefined)
 
   const [uri, setUri] = useState<string>()
-  console.log(rpcSession)
+
   const fetchInteractiveGoals = () => {
     if (editor && rpcSession) {
       const pos = toLanguageServerPosition(editor.getPosition())
@@ -62,20 +62,22 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
   }
 
   const checkCompleted = () => {
-    const pos = toLanguageServerPosition(editor.getPosition())
-    // Get all diagnostics independent of cursor position
-    leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getDiagnostics",
-      "params":{"textDocument":{uri},},
-      "sessionId":rpcSession,
-      "textDocument":{uri},
-      "position": pos
-    }).then((res) => {
-      // Check that there are no errors and no warnings
-      setCompleted(!res.some(({severity}) => severity <= 2))
-      setGlobalDiagnostics(res)
-    }).catch((err) => {
-      console.error(err)
-    })
+    if (editor && rpcSession) {
+      const pos = toLanguageServerPosition(editor.getPosition())
+      // Get all diagnostics independent of cursor position
+      leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getDiagnostics",
+        "params":{"textDocument":{uri},},
+        "sessionId":rpcSession,
+        "textDocument":{uri},
+        "position": pos
+      }).then((res) => {
+        // Check that there are no errors and no warnings
+        setCompleted(!res.some(({severity}) => severity <= 2))
+        setGlobalDiagnostics(res)
+      }).catch((err) => {
+        console.error(err)
+      })
+    }
   }
 
   useEffect(() => {
@@ -84,6 +86,7 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
       checkCompleted()
       const t = editor.onDidChangeModel((ev) => {
         if (ev.newModelUrl) {
+          editorApi.closeRpcSession(rpcSession)
           setRpcSession(undefined)
           setUri(ev.newModelUrl.toString())
           editorApi.createRpcSession(ev.newModelUrl.toString()).then((rpcSession) => {

client/src/components/Level.tsx

@@ -17,10 +17,10 @@ import 'lean4web/client/src/editor/infoview.css'
 import { renderInfoview } from '@leanprover/infoview'
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import './level.css'
-import { ConnectionContext } from '../connection';
+import { ConnectionContext, useLeanClient } 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';
@@ -100,8 +100,6 @@ function Level() {
   const levelId = parseInt(params.levelId)
   const worldId = params.worldId
 
-  const [expertInfoview, setExpertInfoview] = useState(false)
-
   const codeviewRef = useRef<HTMLDivElement>(null)
   const infoviewRef = useRef<HTMLDivElement>(null)
   const messagePanelRef = useRef<HTMLDivElement>(null)
@@ -121,6 +119,8 @@ function Level() {
 
   const connection = React.useContext(ConnectionContext)
 
+  const gameInfo = useGetGameInfoQuery()
+
   const level = useLoadLevelQuery({world: worldId, level: levelId})
 
   const dispatch = useAppDispatch()
@@ -132,7 +132,7 @@ function Level() {
   const initialCode = useSelector(selectCode(worldId, levelId))
 
   const {editor, infoProvider} =
-    useLevelEditor(worldId, levelId, codeviewRef, infoviewRef, initialCode, onDidChangeContent)
+    useLevelEditor(worldId, levelId, codeviewRef, initialCode, onDidChangeContent)
 
   const {setTitle, setSubtitle} = React.useContext(SetTitleContext);
 
@@ -171,15 +171,9 @@ 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' }}>
-            <Infoview leanClient={connection.getLeanClient()} editor={editor} editorApi={infoProvider?.getApi()} />
-          </div>
-          <FormGroup>
-            <FormControlLabel onChange={() => { setExpertInfoview(!expertInfoview) }} control={<Switch />} label="Expert mode" />
-          </FormGroup>
+          <Infoview leanClient={connection.getLeanClient()} editor={editor} editorApi={infoProvider?.getApi()} />
         </Grid>
       </Grid>
     </Box>
@@ -189,13 +183,12 @@ function Level() {
 export default Level
 
 
-function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewRef, initialCode, onDidChangeContent) {
+function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCode, onDidChangeContent) {
 
   const connection = React.useContext(ConnectionContext)
 
   const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
   const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
-  const [infoviewApi, setInfoviewApi] = useState(null)
 
   // Create Editor
   useEffect(() => {
@@ -217,38 +210,32 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewR
     })
 
     const infoProvider = new InfoProvider(connection.getLeanClient())
-    const div: HTMLElement = infoviewRef.current!
-    const infoviewApi = renderInfoview(infoProvider.getApi(), div)
-
+console.log()
     setEditor(editor)
     setInfoProvider(infoProvider)
-    setInfoviewApi(infoviewApi)
 
     return () => { editor.setModel(null); infoProvider.dispose(); editor.dispose() }
   }, [])
 
+  const {leanClient, leanClientStarted} = useLeanClient()
+
   // Create model when level changes
   useEffect(() => {
-    connection.startLeanClient().then((leanClient) => {
-      if (editor) {
-
-        const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`)
-        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)
-        infoProvider.openPreview(editor, infoviewApi)
-        new LeanTaskGutter(infoProvider.client, editor)
-
-        new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
+    if (editor && leanClientStarted) {
+
+      const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`)
+      let model = monaco.editor.getModel(uri)
+      if (!model) {
+        model = monaco.editor.createModel(initialCode, 'lean4', uri)
+        model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
       }
-    })
-    // TODO: Properly close the file to stop send "keepAlive" calls to the server
-  }, [editor, levelId, connection])
+      editor.setModel(model)
+      const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
+      const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
+
+      return () => { abbrevRewriter.dispose(); taskGutter.dispose(); model.dispose() }
+    }
+  }, [editor, levelId, connection, leanClientStarted])
 
   return {editor, infoProvider}
 }

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" strokeWidth="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",  textAnchor: "middle", dominantBaseline: "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) =>
-            <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>)}
+          {svgElements}
         </svg>
       </Box>
     </div>

client/src/connection.ts

@@ -2,12 +2,13 @@
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { LeanClient } from 'lean4web/client/src/editor/leanclient';
 import * as React from 'react';
+import { useState } from 'react';
 
 
 export class Connection {
   private leanClient = null
 
-  getLeanClient() {
+  getLeanClient(): LeanClient {
     if (this.leanClient === null) {
       const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/'
 
@@ -30,7 +31,7 @@ export class Connection {
         if (!leanClient.isStarted()) {
           leanClient.start()
         }
-       leanClient.restarted(() => { resolve(leanClient) })
+        leanClient.restarted(() => { resolve(leanClient) })
       }
     })
   }
@@ -39,3 +40,11 @@ export class Connection {
 export const connection = new Connection()
 
 export const ConnectionContext = React.createContext(null);
+
+export const useLeanClient = () => {
+  const leanClient = connection.getLeanClient()
+  const [leanClientStarted, setLeanClientStarted] = useState(leanClient.isStarted())
+  leanClient.restarted(() => { setLeanClientStarted(true) })
+  // TODO handle stopping lean client
+  return {leanClientStarted, leanClient}
+}

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,
 }

package.json

@@ -4,6 +4,8 @@
   "private": true,
   "homepage": ".",
   "dependencies": {
+    "@emotion/react": "^11.10.5",
+    "@emotion/styled": "^11.10.5",
     "@fontsource/roboto": "^4.5.8",
     "@fontsource/roboto-mono": "^4.5.8",
     "@mui/icons-material": "^5.10.6",

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
-\"Next Level\" klicken
+- Keine Möglichkeit zurück zu gehen
 - Fehlermeldungen sind nicht besonders Benutzerfreundlich: Ganz unverständliche sammeln,
 damit wir diese später modifizieren können.
 - Kann man Taktiken blockieren?