diff --git a/client/src/components/Infoview.tsx b/client/src/components/Infoview.tsx index 4f016c7..39fee9b 100644 --- a/client/src/components/Infoview.tsx +++ b/client/src/components/Infoview.tsx @@ -25,7 +25,7 @@ function Infoview({ editor, editorApi, leanClient } : {editor: monaco.editor.ISt const [globalDiagnostics, setGlobalDiagnostics] = useState(undefined) const [uri, setUri] = useState() - console.log(rpcSession) + const fetchInteractiveGoals = () => { if (editor && rpcSession) { const pos = toLanguageServerPosition(editor.getPosition()) @@ -84,6 +84,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) => {