From 02501613b4ed6c60adb4c2c8a2dc50f7e1699a86 Mon Sep 17 00:00:00 2001 From: zqy1018 Date: Mon, 12 Dec 2022 17:43:36 +0800 Subject: [PATCH 1/3] Added a message view panel. --- client/src/CoqDocument.ts | 8 +- client/src/HtmlCoqView.ts | 8 +- client/src/protocol.ts | 10 ++ html_views/src/goals/display-proof-state.ts | 36 +++++++ html_views/src/goals/proof-view.css | 106 ++++++++++++++++---- html_views/src/goals/protocol.ts | 10 ++ 6 files changed, 155 insertions(+), 23 deletions(-) diff --git a/client/src/CoqDocument.ts b/client/src/CoqDocument.ts index d86a9a84..06d78c77 100644 --- a/client/src/CoqDocument.ts +++ b/client/src/CoqDocument.ts @@ -175,7 +175,10 @@ export class CoqDocument implements vscode.Disposable { private onCoqMessage(params: proto.NotifyMessageParams) { if (params.routeId == this.queryRouteId) { this.project.queryOut.show(true); - this.project.queryOut.appendLine(psm.prettyTextToString(params.message)); + const processedMessage = psm.prettyTextToString(params.message); + this.project.queryOut.appendLine(processedMessage); + // send the same message to the message panel + this.view.update({ innertext: params.message, type: "message-query" }); } else { switch (params.level) { case 'warning': @@ -358,7 +361,7 @@ export class CoqDocument implements vscode.Disposable { } } else if(value.type === 'interrupted') this.statusBar.setStateComputing(proto.ComputingStatus.Interrupted) - else + else if (value.type !== 'message-query' && value.type !== 'message-clear') this.updateFocus(value.focus, this.project.settings.moveCursorToFocus); return true; @@ -479,6 +482,7 @@ export class CoqDocument implements vscode.Disposable { try { if (term) { this.project.queryOut.clear(); + this.view.update({ type:"message-clear" }); this.project.queryOut.show(true); this.langServer.query(query, term, this.queryRouteId); } diff --git a/client/src/HtmlCoqView.ts b/client/src/HtmlCoqView.ts index 70b2bbfa..341c36f8 100644 --- a/client/src/HtmlCoqView.ts +++ b/client/src/HtmlCoqView.ts @@ -41,7 +41,12 @@ interface SettingsState { proofViewDiff?: ProofViewDiffSettings; } -type ProofViewProtocol = GoalUpdate | SettingsUpdate; +interface QueryMessageUpdate { + command: "message-query"; + msg: string +} + +type ProofViewProtocol = GoalUpdate | SettingsUpdate | QueryMessageUpdate; const VIEW_PATH = "html_views"; @@ -146,6 +151,7 @@ export class HtmlCoqView implements view.CoqView { }, { enableScripts: true, + enableFindWidget: true } ); diff --git a/client/src/protocol.ts b/client/src/protocol.ts index 18fcb9f6..4203072e 100644 --- a/client/src/protocol.ts +++ b/client/src/protocol.ts @@ -164,6 +164,10 @@ export interface CommandInterrupted { range: vscode.Range } +export interface QueryMessageWrapper { + innertext: AnnotatedText +} + export type FocusPosition = {focus: vscode.Position} export type NotRunningTag = {type: 'not-running'} export type NoProofTag = {type: 'no-proof'} @@ -171,13 +175,19 @@ export type FailureTag = {type: 'failure'} export type ProofViewTag = {type: 'proof-view'} export type InterruptedTag = {type: 'interrupted'} export type BusyTag = {type: 'busy'} +export type QueryMessageTag = {type: 'message-query'} +export type ClearMessageTag = {type: 'message-clear'} export type NotRunningResult = NotRunningTag & {reason: "not-started"|"spawn-failed", coqtop?: string} export type BusyResult = BusyTag export type NoProofResult = NoProofTag export type FailureResult = FailValue & FailureTag export type ProofViewResult = ProofView & ProofViewTag export type InterruptedResult = CommandInterrupted & InterruptedTag +export type QueryMessageResult = QueryMessageWrapper & QueryMessageTag +export type ClearMessageResult = ClearMessageTag export type CommandResult = + QueryMessageResult | + ClearMessageResult | NotRunningResult | (BusyResult & FocusPosition) | (FailureResult & FocusPosition) | diff --git a/html_views/src/goals/display-proof-state.ts b/html_views/src/goals/display-proof-state.ts index 42906e95..43967aac 100644 --- a/html_views/src/goals/display-proof-state.ts +++ b/html_views/src/goals/display-proof-state.ts @@ -232,10 +232,33 @@ export const ProofState = () => { return { element, updateState, unmount }; }; +export const OtherInfoView = () => { + const queryView = h("vscode-panel-view"); + const element = h("vscode-panels.panels", [ + h("vscode-panel-tab", "QUERY"), + queryView + ]); + + let queryViewInnerDiv = h("pre.richpp"); + queryView.appendChild(queryViewInnerDiv); + + const resetInnerMessage = () => { + queryViewInnerDiv.innerHTML = ""; + }; + + const updateInnerMessage = (s : AnnotatedText) => { + queryViewInnerDiv.appendChild(h("ul", createAnnotatedText(s))); + }; + + return { element, updateInnerMessage, resetInnerMessage }; +}; + export const Infoview = () => { const element = h("div"); let proofStateInstance: ReturnType | undefined = undefined; + let otherViewInstance = OtherInfoView(); + let divider = h("vscode-divider"); const updateState = (state: CommandResult) => { if (state.type === "proof-view") { @@ -243,9 +266,18 @@ export const Infoview = () => { element.innerHTML = ""; proofStateInstance = ProofState(); element.appendChild(proofStateInstance.element); + element.appendChild(divider); + element.appendChild(otherViewInstance.element); } proofStateInstance.updateState(state); + } else if (state.type === "message-query") { + // if (state.innertext) + otherViewInstance.updateInnerMessage(state.innertext); + // else + // otherViewInstance.updateInnerMessage("nothing. why?"); + } else if (state.type === "message-clear") { + otherViewInstance.resetInnerMessage(); } else { if (proofStateInstance !== undefined) { proofStateInstance.unmount(); @@ -257,6 +289,8 @@ export const Infoview = () => { element.innerHTML = ""; const formatted = h("div.message", message); element.appendChild(formatted); + element.appendChild(divider); + element.appendChild(otherViewInstance.element); }; const setErrorMessage = (message: HTMLElement) => { @@ -266,6 +300,8 @@ export const Infoview = () => { h("code", message), ]); element.appendChild(formatted); + element.appendChild(divider); + element.appendChild(otherViewInstance.element); }; if (state.type === "not-running") { diff --git a/html_views/src/goals/proof-view.css b/html_views/src/goals/proof-view.css index b7eb5d66..3df54120 100644 --- a/html_views/src/goals/proof-view.css +++ b/html_views/src/goals/proof-view.css @@ -215,49 +215,79 @@ span[class~=charsRemoved][class~=substitution]::before { border-top-color: var(--vscode-coq-subgoalSeparator); } -.richpp .constr-notation { - color: var(--vscode-coq-termNotation); + +/* complying with the order of https://github.com/coq/coq/blob/master/ide/coqide/preferences.ml */ +/* FIXME: need to put this part into package.json */ +.richpp .constr-evar { + color: var(--vscode-coq-termEvarColor); + font-weight: var(--vscode-coq-termEvarFontWeight); + font-style: italic; } .richpp .constr-keyword { - color: var(--vscode-coq-termKeyword); + color: var(--vscode-coq-termKeywordColor); + /* font-weight: var(--vscode-coq-termKeywordFontWeight); */ + font-weight:normal } -.richpp .constr-evar { - color: var(--vscode-coq-termEvar); - font-style: italic; +.richpp .constr-type { + color: var(--vscode-coq-termTypeColor); + font-weight: var(--vscode-coq-termTypeFontWeight); } -.richpp .constr-path { - color: var(--vscode-coq-termPath); +.richpp .constr-notation { + color: var(--vscode-coq-termNotationColor); + font-weight: var(--vscode-coq-termNotationFontWeight); } .richpp .constr-reference { - color: var(--vscode-coq-termReference); + color: var(--vscode-coq-termReferenceColor); + font-weight: var(--vscode-coq-termReferenceFontWeight); } -.richpp .constr-type { - color: var(--vscode-coq-termType); +.richpp .constr-path { + color: var(--vscode-coq-termPathColor); + font-weight: var(--vscode-coq-termPathFontWeight); } .richpp .constr-variable { - color: var(--vscode-coq-termVariable); + color: var(--vscode-coq-termVariableColor); + font-weight: var(--vscode-coq-termVariableFontWeight); } .richpp .message-debug { - color: var(--vscode-coq-debugMessage); + color: var(--vscode-coq-debugMessageColor); + font-weight: var(--vscode-coq-debugMessageFontWeight); } .richpp .message-error { - color: var(--vscode-coq-errorMessage); + color: var(--vscode-coq-errorMessageColor); + font-weight: var(--vscode-coq-errorMessageFontWeight); text-decoration: underline; } .richpp .message-warning { - color: var(--vscode-coq-warningMessage); + color: var(--vscode-coq-warningMessageColor); + font-weight: var(--vscode-coq-warningMessageFontWeight); +} +.richpp .message-prompt { + color: var(--vscode-coq-promptMessageColor); + font-weight: var(--vscode-coq-promptMessageFontWeight); +} +.richpp .module-definition { + color: var(--vscode-coq-moduleDefinitionColor); + font-weight: var(--vscode-coq-moduleDefinitionFontWeight); } .richpp .module-keyword { - color: var(--vscode-coq-moduleKeyword); + color: var(--vscode-coq-moduleKeywordColor); + font-weight: var(--vscode-coq-moduleKeywordFontWeight); } .richpp .tactic-keyword { - color: var(--vscode-coq-tacticKeyword); + color: var(--vscode-coq-tacticKeywordColor); + font-weight: var(--vscode-coq-tacticKeywordFontWeight); } .richpp .tactic-primitive { - color: var(--vscode-coq-tacticPrimitive); + color: var(--vscode-coq-tacticPrimitiveColor); + font-weight: var(--vscode-coq-tacticPrimitiveFontWeight); } .richpp .tactic-string { - color: var(--vscode-coq-tacticString); + color: var(--vscode-coq-tacticStringColor); + font-weight: var(--vscode-coq-tacticStringFontWeight); +} + +pre { + font-family: var(--vscode-editor-font-family); } .panels { @@ -279,4 +309,40 @@ vscode-panel-tab { .given-up-goals-warning { padding-bottom: 10px; -} \ No newline at end of file +} + +:root { + --vscode-coq-termEvarColor:initial; + --vscode-coq-termEvarFontWeight:initial; + --vscode-coq-termKeywordColor:rgb(0, 173, 0); + --vscode-coq-termKeywordFontWeight:bold; + --vscode-coq-termTypeColor:orange; + --vscode-coq-termTypeFontWeight:bold; + --vscode-coq-termNotationColor:chocolate; + --vscode-coq-termNotationFontWeight:initial; + --vscode-coq-termReferenceColor:rgb(0, 173, 0); + --vscode-coq-termReferenceFontWeight:initial; + --vscode-coq-termPathColor:blueviolet; + --vscode-coq-termPathFontWeight:initial; + --vscode-coq-termVariableColor:initial; + --vscode-coq-termVariableFontWeight:initial; + --vscode-coq-debugMessageColor:initial; + --vscode-coq-debugMessageFontWeight:initial; + --vscode-coq-errorMessageColor:initial; + --vscode-coq-errorMessageFontWeight:initial; + --vscode-coq-warningMessageColor:initial; + --vscode-coq-warningMessageFontWeight:initial; + --vscode-coq-promptMessageColor:initial; + --vscode-coq-promptMessageFontWeight:initial; + --vscode-coq-moduleDefinitionColor:orangered; + --vscode-coq-moduleDefinitionFontWeight:bold; + --vscode-coq-moduleKeywordColor:initial; + --vscode-coq-moduleKeywordFontWeight:initial; + --vscode-coq-tacticKeywordColor:initial; + --vscode-coq-tacticKeywordFontWeight:initial; + --vscode-coq-tacticPrimitiveColor:initial; + --vscode-coq-tacticPrimitiveFontWeight:initial; + --vscode-coq-tacticStringColor:initial; + --vscode-coq-tacticStringFontWeight:initial; + --vscode-coq-hypothesisIdent:lime; +} diff --git a/html_views/src/goals/protocol.ts b/html_views/src/goals/protocol.ts index b59210c9..9d888e50 100644 --- a/html_views/src/goals/protocol.ts +++ b/html_views/src/goals/protocol.ts @@ -92,17 +92,27 @@ interface CommandInterrupted { range: any } +export interface QueryMessageWrapper { + innertext: AnnotatedText +} + type FocusPosition = {focus: any} type NotRunningTag = {type: 'not-running'} type NoProofTag = {type: 'no-proof'} type FailureTag = {type: 'failure'} type ProofViewTag = {type: 'proof-view'} type InterruptedTag = {type: 'interrupted'} +type QueryMessageTag = {type: 'message-query'} +type ClearMessageTag = {type: 'message-clear'} type NoProofResult = NoProofTag type FailureResult = FailValue & FailureTag type ProofViewResult = ProofView & ProofViewTag type InterruptedResult = CommandInterrupted & InterruptedTag +type QueryMessageResult = QueryMessageWrapper & QueryMessageTag +type ClearMessageResult = ClearMessageTag export type CommandResult = + QueryMessageResult | + ClearMessageResult | NotRunningTag | (FailureResult & FocusPosition) | (ProofViewResult & FocusPosition) | From a59acd5d7fc59b43b013a5a89e8f9bb9cfd41505 Mon Sep 17 00:00:00 2001 From: zqy1018 Date: Wed, 14 Dec 2022 23:54:18 +0800 Subject: [PATCH 2/3] Relay all output to message panel; clear-on-demand --- client/src/CoqDocument.ts | 12 +++++-- client/src/protocol.ts | 6 ++-- html_views/src/goals/display-proof-state.ts | 35 ++++++++++++++------- html_views/src/goals/protocol.ts | 6 ++-- 4 files changed, 39 insertions(+), 20 deletions(-) diff --git a/client/src/CoqDocument.ts b/client/src/CoqDocument.ts index 06d78c77..23268e82 100644 --- a/client/src/CoqDocument.ts +++ b/client/src/CoqDocument.ts @@ -184,18 +184,22 @@ export class CoqDocument implements vscode.Disposable { case 'warning': this.project.infoOut.show(true); this.project.infoOut.appendLine(psm.prettyTextToString(params.message)); + this.view.update({ innertext: params.message, type: "message-query" }); return; case 'info': this.project.infoOut.appendLine(psm.prettyTextToString(params.message)); + this.view.update({ innertext: params.message, type: "message-query" }); return; case 'notice': this.project.noticeOut.show(true); this.project.noticeOut.append(psm.prettyTextToString(params.message)); this.project.noticeOut.append("\n"); + this.view.update({ innertext: params.message, type: "message-query" }); return; case 'debug': this.project.debugOut.show(true); this.project.debugOut.appendLine(psm.prettyTextToString(params.message)); + this.view.update({ innertext: params.message, type: "message-query" }); return; } } @@ -361,7 +365,7 @@ export class CoqDocument implements vscode.Disposable { } } else if(value.type === 'interrupted') this.statusBar.setStateComputing(proto.ComputingStatus.Interrupted) - else if (value.type !== 'message-query' && value.type !== 'message-clear') + else if (value.type !== 'message-query' && value.type !== 'message-ready-clear') this.updateFocus(value.focus, this.project.settings.moveCursorToFocus); return true; @@ -418,6 +422,7 @@ export class CoqDocument implements vscode.Disposable { try { this.makePreviewOpenedFilePermanent(editor); this.rememberCursors(); + this.view.update({ type:"message-ready-clear" }); const value = await this.langServer.stepForward(); this.updateView(value, true); this.handleResult(value); @@ -444,6 +449,7 @@ export class CoqDocument implements vscode.Disposable { public async finishComputations(editor: TextEditor) { this.statusBar.setStateWorking('Finishing computations'); try { + this.view.update({ type:"message-ready-clear" }); await this.langServer.finishComputations(); this.statusBar.setStateReady(); } catch (err) { @@ -456,6 +462,7 @@ export class CoqDocument implements vscode.Disposable { if(!editor || editor.document.uri.toString() !== this.documentUri) return; this.makePreviewOpenedFilePermanent(editor); + this.view.update({ type:"message-ready-clear" }); const value = await this.langServer.interpretToPoint(editor.selection.active, synchronous); this.updateView(value, true); this.handleResult(value); @@ -471,6 +478,7 @@ export class CoqDocument implements vscode.Disposable { this.statusBar.setStateWorking('Interpreting to end'); try { this.makePreviewOpenedFilePermanent(editor); + this.view.update({ type:"message-ready-clear" }); const value = await this.langServer.interpretToEnd(synchronous); this.updateView(value, true); this.handleResult(value); @@ -482,7 +490,7 @@ export class CoqDocument implements vscode.Disposable { try { if (term) { this.project.queryOut.clear(); - this.view.update({ type:"message-clear" }); + this.view.update({ type:"message-ready-clear" }); this.project.queryOut.show(true); this.langServer.query(query, term, this.queryRouteId); } diff --git a/client/src/protocol.ts b/client/src/protocol.ts index 4203072e..365a5287 100644 --- a/client/src/protocol.ts +++ b/client/src/protocol.ts @@ -176,7 +176,7 @@ export type ProofViewTag = {type: 'proof-view'} export type InterruptedTag = {type: 'interrupted'} export type BusyTag = {type: 'busy'} export type QueryMessageTag = {type: 'message-query'} -export type ClearMessageTag = {type: 'message-clear'} +export type ReadyClearMessageTag = {type: 'message-ready-clear'} export type NotRunningResult = NotRunningTag & {reason: "not-started"|"spawn-failed", coqtop?: string} export type BusyResult = BusyTag export type NoProofResult = NoProofTag @@ -184,10 +184,10 @@ export type FailureResult = FailValue & FailureTag export type ProofViewResult = ProofView & ProofViewTag export type InterruptedResult = CommandInterrupted & InterruptedTag export type QueryMessageResult = QueryMessageWrapper & QueryMessageTag -export type ClearMessageResult = ClearMessageTag +export type ReadyClearMessageResult = ReadyClearMessageTag export type CommandResult = QueryMessageResult | - ClearMessageResult | + ReadyClearMessageResult | NotRunningResult | (BusyResult & FocusPosition) | (FailureResult & FocusPosition) | diff --git a/html_views/src/goals/display-proof-state.ts b/html_views/src/goals/display-proof-state.ts index 43967aac..6c037b6f 100644 --- a/html_views/src/goals/display-proof-state.ts +++ b/html_views/src/goals/display-proof-state.ts @@ -233,24 +233,35 @@ export const ProofState = () => { }; export const OtherInfoView = () => { - const queryView = h("vscode-panel-view"); + const messageView = h("vscode-panel-view"); const element = h("vscode-panels.panels", [ - h("vscode-panel-tab", "QUERY"), - queryView + h("vscode-panel-tab", "MESSAGE"), + messageView ]); - let queryViewInnerDiv = h("pre.richpp"); - queryView.appendChild(queryViewInnerDiv); - - const resetInnerMessage = () => { - queryViewInnerDiv.innerHTML = ""; + let messageViewInnerDiv = h("pre"); + messageView.appendChild(messageViewInnerDiv); + + /* + clear-on-demand: + if this flag is set, the message panel will be reset on receiving the next incoming message + and this flag will be unset immediately after that + */ + let ready : boolean = true; + + const readyForMessageReset = () => { + ready = true; }; const updateInnerMessage = (s : AnnotatedText) => { - queryViewInnerDiv.appendChild(h("ul", createAnnotatedText(s))); + if (ready){ + messageViewInnerDiv.innerHTML = ""; + ready = false; + } + messageViewInnerDiv.appendChild(h("span", [...createAnnotatedText(s), "\n"])); }; - return { element, updateInnerMessage, resetInnerMessage }; + return { element, updateInnerMessage, readyForMessageReset }; }; export const Infoview = () => { @@ -276,8 +287,8 @@ export const Infoview = () => { otherViewInstance.updateInnerMessage(state.innertext); // else // otherViewInstance.updateInnerMessage("nothing. why?"); - } else if (state.type === "message-clear") { - otherViewInstance.resetInnerMessage(); + } else if (state.type === "message-ready-clear") { + otherViewInstance.readyForMessageReset(); } else { if (proofStateInstance !== undefined) { proofStateInstance.unmount(); diff --git a/html_views/src/goals/protocol.ts b/html_views/src/goals/protocol.ts index 9d888e50..7cc6ca3c 100644 --- a/html_views/src/goals/protocol.ts +++ b/html_views/src/goals/protocol.ts @@ -103,16 +103,16 @@ type FailureTag = {type: 'failure'} type ProofViewTag = {type: 'proof-view'} type InterruptedTag = {type: 'interrupted'} type QueryMessageTag = {type: 'message-query'} -type ClearMessageTag = {type: 'message-clear'} +type ReadyClearMessageTag = {type: 'message-ready-clear'} type NoProofResult = NoProofTag type FailureResult = FailValue & FailureTag type ProofViewResult = ProofView & ProofViewTag type InterruptedResult = CommandInterrupted & InterruptedTag type QueryMessageResult = QueryMessageWrapper & QueryMessageTag -type ClearMessageResult = ClearMessageTag +type ReadyClearMessageResult = ReadyClearMessageTag export type CommandResult = QueryMessageResult | - ClearMessageResult | + ReadyClearMessageResult | NotRunningTag | (FailureResult & FocusPosition) | (ProofViewResult & FocusPosition) | From 3421d174c3f3a940ffc59c4c1aaa06e2b081726e Mon Sep 17 00:00:00 2001 From: zqy1018 Date: Wed, 14 Dec 2022 23:58:22 +0800 Subject: [PATCH 3/3] Commented out things related to output channels --- client/src/CoqDocument.ts | 9 ++++++--- client/src/CoqProject.ts | 6 ++++++ 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/client/src/CoqDocument.ts b/client/src/CoqDocument.ts index 23268e82..9263046c 100644 --- a/client/src/CoqDocument.ts +++ b/client/src/CoqDocument.ts @@ -20,7 +20,7 @@ import {CoqDocumentLanguageServer} from './CoqLanguageServer'; import {CoqView, adjacentPane} from './CoqView'; import {StatusBar} from './StatusBar'; import {CoqProject} from './CoqProject'; -import * as psm from './prettify-symbols-mode'; +// import * as psm from './prettify-symbols-mode'; namespace DisplayOptionPicks { type T = vscode.QuickPickItem & {displayItem: number}; @@ -173,6 +173,8 @@ export class CoqDocument implements vscode.Disposable { // } private onCoqMessage(params: proto.NotifyMessageParams) { + this.view.update({ innertext: params.message, type: "message-query" }); + /* if (params.routeId == this.queryRouteId) { this.project.queryOut.show(true); const processedMessage = psm.prettyTextToString(params.message); @@ -203,6 +205,7 @@ export class CoqDocument implements vscode.Disposable { return; } } + */ } @@ -489,9 +492,9 @@ export class CoqDocument implements vscode.Disposable { public async query(query: proto.QueryFunction, term: string | undefined) { try { if (term) { - this.project.queryOut.clear(); + // this.project.queryOut.clear(); this.view.update({ type:"message-ready-clear" }); - this.project.queryOut.show(true); + // this.project.queryOut.show(true); this.langServer.query(query, term, this.queryRouteId); } } catch (err) { diff --git a/client/src/CoqProject.ts b/client/src/CoqProject.ts index 43252786..50f011c0 100644 --- a/client/src/CoqProject.ts +++ b/client/src/CoqProject.ts @@ -26,10 +26,12 @@ export class CoqProject implements vscode.Disposable { private subscriptions : vscode.Disposable[] = []; // lazily created output windows + /* private infoOutput: vscode.OutputChannel = vscode.window.createOutputChannel('Info'); private queryOutput: vscode.OutputChannel = vscode.window.createOutputChannel('Queries'); private noticeOutput: vscode.OutputChannel = vscode.window.createOutputChannel('Notices'); private debugOutput: vscode.OutputChannel = vscode.window.createOutputChannel('Debug'); + */ private constructor(context: vscode.ExtensionContext) { this.langServer = CoqLanguageServer.create(context); @@ -70,6 +72,7 @@ export class CoqProject implements vscode.Disposable { return CoqProject.instance; } + /* public get infoOut(): vscode.OutputChannel { return this.infoOutput; } @@ -82,11 +85,14 @@ export class CoqProject implements vscode.Disposable { public get debugOut(): vscode.OutputChannel { return this.debugOutput; } + */ dispose() { + /* this.infoOutput.dispose(); this.queryOutput.dispose(); this.noticeOutput.dispose(); + */ this.documents.forEach((doc) => doc.dispose()); this.subscriptions.forEach((s) => s.dispose()); this.langServer.dispose();