close rpc sessions properly
This commit is contained in:
@@ -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())
|
||||
@@ -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) => {
|
||||
|
||||
Reference in New Issue
Block a user