unmount editor properly

client/src/components/Infoview.tsx

@@ -62,20 +62,22 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
   }
 
   const checkCompleted = () => {
-    const pos = toLanguageServerPosition(editor.getPosition())
+    if (editor && rpcSession) {
-    // Get all diagnostics independent of cursor position
+      const pos = toLanguageServerPosition(editor.getPosition())
-    leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getDiagnostics",
+      // Get all diagnostics independent of cursor position
-      "params":{"textDocument":{uri},},
+      leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getDiagnostics",
-      "sessionId":rpcSession,
+        "params":{"textDocument":{uri},},
-      "textDocument":{uri},
+        "sessionId":rpcSession,
-      "position": pos
+        "textDocument":{uri},
-    }).then((res) => {
+        "position": pos
-      // Check that there are no errors and no warnings
+      }).then((res) => {
-      setCompleted(!res.some(({severity}) => severity <= 2))
+        // Check that there are no errors and no warnings
-      setGlobalDiagnostics(res)
+        setCompleted(!res.some(({severity}) => severity <= 2))
-    }).catch((err) => {
+        setGlobalDiagnostics(res)
-      console.error(err)
+      }).catch((err) => {
-    })
+        console.error(err)
+      })
+    }
   }
 
   useEffect(() => {

client/src/components/Level.tsx

@@ -17,7 +17,7 @@ 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 { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api';
@@ -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)
@@ -134,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);
 
@@ -175,13 +173,7 @@ function Level() {
           <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={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>
+          <Infoview leanClient={connection.getLeanClient()} editor={editor} editorApi={infoProvider?.getApi()} />
-          <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>
         </Grid>
       </Grid>
     </Box>
@@ -191,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(() => {
@@ -219,38 +210,32 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, infoviewR
     })
 
     const infoProvider = new InfoProvider(connection.getLeanClient())
-    const div: HTMLElement = infoviewRef.current!
+console.log()
-    const infoviewApi = renderInfoview(infoProvider.getApi(), div)
-
     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 && leanClientStarted) {
-      if (editor) {
+
-
+      const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`)
-        const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`)
+      let model = monaco.editor.getModel(uri)
-        let model = monaco.editor.getModel(uri)
+      if (!model) {
-        if (!model) {
+        model = monaco.editor.createModel(initialCode, 'lean4', uri)
-          model = monaco.editor.createModel(initialCode, 'lean4', uri)
+        model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
-          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)
       }
-    })
+      editor.setModel(model)
-    // TODO: Properly close the file to stop send "keepAlive" calls to the server
+      const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
-  }, [editor, levelId, connection])
+      const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
+
+      return () => { abbrevRewriter.dispose(); taskGutter.dispose(); model.dispose() }
+    }
+  }, [editor, levelId, connection, leanClientStarted])
 
   return {editor, infoProvider}
 }

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

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