useEditorUri, hide server crash messages

client/src/components/Infoview.tsx

@@ -5,13 +5,14 @@ import { LeanClient } from 'lean4web/client/src/editor/leanclient';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import * as ls from 'vscode-languageserver-protocol'
 import TacticState from './TacticState';
+import { useLeanClient } from '../connection';
 
 // TODO: move into Lean 4 web
 function toLanguageServerPosition (pos: monaco.Position): ls.Position {
   return {line : pos.lineNumber - 1, character: pos.column - 1}
 }
 
-function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.IStandaloneCodeEditor, editorApi: EditorApi, leanClient: LeanClient}) {
+function Infoview({ editor, editorApi } : {editor: monaco.editor.IStandaloneCodeEditor, editorApi: EditorApi}) {
   const [rpcSession, setRpcSession] = useState<string>()
   const [goals, setGoals] = useState<any[]>(null)
   const [completed, setCompleted] = useState<boolean>(false)
@@ -24,10 +25,11 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
   isn't complete. */
   const [globalDiagnostics, setGlobalDiagnostics] = useState<any[]>(undefined)
 
-  const [uri, setUri] = useState<string>()
+  const {uri} = useEditorUri(editor)
+  const {leanClient, leanClientStarted} = useLeanClient()
 
   const fetchInteractiveGoals = () => {
-    if (editor && rpcSession) {
+    if (editor && rpcSession && editor.getPosition()) {
       const pos = toLanguageServerPosition(editor.getPosition())
 
       leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getGoals",
@@ -62,7 +64,7 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
   }
 
   const checkCompleted = () => {
-    if (editor && rpcSession) {
+    if (editor && rpcSession && editor.getPosition()) {
       const pos = toLanguageServerPosition(editor.getPosition())
       // Get all diagnostics independent of cursor position
       leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getDiagnostics",
@@ -84,19 +86,19 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
     if (editor) {
       fetchInteractiveGoals()
       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) => {
-            setRpcSession(rpcSession)
-          })
-        }
+    }
+  }, [editor, uri, rpcSession]);
+
+  useEffect(() => {
+    if (editorApi && leanClientStarted && uri) {
+      editorApi.closeRpcSession(rpcSession)
+      setRpcSession(undefined)
+      console.log(uri)
+      editorApi.createRpcSession(uri).then((rpcSession) => {
+        setRpcSession(rpcSession)
       })
-      return () => {t.dispose()}
     }
-  }, [editor, rpcSession]);
+  }, [editorApi, uri]);
 
   useEffect(() => {
     if (editor) {
@@ -122,3 +124,22 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt
 }
 
 export default Infoview
+
+const useEditorUri = (editor: monaco.editor.IStandaloneCodeEditor) => {
+  const [uri, setUri] = useState<string>(undefined)
+
+  useEffect(() => {
+    if (editor) {
+      const t = editor.onDidChangeModel((ev) => {
+        if (ev.newModelUrl) {
+          setUri(ev.newModelUrl.toString())
+        } else {
+          setUri(undefined)
+        }
+      })
+      return () => {t.dispose()}
+    }
+  }, [editor])
+
+  return {uri}
+}

client/src/components/Level.tsx

@@ -14,7 +14,6 @@ import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/Ab
 import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
 import { InfoProvider } from 'lean4web/client/src/editor/infoview';
 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, useLeanClient } from '../connection';
@@ -177,7 +176,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>
 
-          <Infoview key={worldId + "/Level" + levelId} leanClient={connection.getLeanClient()} editor={editor} editorApi={infoProvider?.getApi()} />
+          <Infoview key={worldId + "/Level" + levelId} editor={editor} editorApi={infoProvider?.getApi()} />
         </Grid>
       </Grid>
     </Box>
@@ -214,7 +213,7 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCo
     })
 
     const infoProvider = new InfoProvider(connection.getLeanClient())
-console.log()
+
     setEditor(editor)
     setInfoProvider(infoProvider)
 

client/src/connection.ts

@@ -44,7 +44,13 @@ 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
+
+  React.useEffect(() => {
+    const t1 = leanClient.restarted(() => { console.log("START"); setLeanClientStarted(true) })
+    const t2 = leanClient.stopped(() => { console.log("STOP"); setLeanClientStarted(false) })
+
+    return () => {t1.dispose(); t2.dispose()}
+  }, [leanClient, setLeanClientStarted])
+
   return {leanClientStarted, leanClient}
 }

client/src/index.css

@@ -19,3 +19,8 @@ code {
 .AppBar {
   flex: 0;
 }
+
+/* Hide monaco editor notifications */
+.monaco-workbench > .notifications-toasts.visible {
+  display: none !important;
+}

package-lock.json

@@ -6049,7 +6049,7 @@
     },
     "node_modules/lean4web": {
       "version": "0.1.0",
-      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#1b6f7c556c075c3906489d2e82ecf262ede1d9c5",
+      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#b887fcd519be50c21a8ca35a6620aaeee6940b6e",
       "dependencies": {
         "@fontsource/roboto": "^4.5.8",
         "@fontsource/roboto-mono": "^4.5.8",