diff --git a/CHANGES.md b/CHANGES.md index 036dc539..54fc5991 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -38,6 +38,8 @@ (@ejgallego, #616) - completion: correctly understand UTF-16 code points on completion request (Léo Stefanesco, #613, fixes #531) + - don't trigger the goals window in general markdown buffer + (@ejgallego, #625, reported by Théo Zimmerman) # coq-lsp 0.1.8: Trick-or-treat ------------------------------- diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index 313e777b..953eff6c 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -12,6 +12,8 @@ import { ThemeColor, WorkspaceConfiguration, Disposable, + DocumentSelector, + languages, } from "vscode"; import { @@ -29,7 +31,11 @@ import { GoalAnswer, PpString, } from "../lib/types"; -import { CoqLspClientConfig, CoqLspServerConfig } from "./config"; +import { + CoqLspClientConfig, + CoqLspServerConfig, + coqLSPDocumentSelector, +} from "./config"; import { InfoPanel, goalReq } from "./goals"; import { FileProgressManager } from "./progress"; import { coqPerfData, PerfDataView } from "./perf"; @@ -208,10 +214,8 @@ export function activateCoqLSP( textEditor: TextEditor, callKind: TextEditorSelectionChangeKind | undefined ) => { - if ( - textEditor.document.languageId != "coq" && - textEditor.document.languageId != "markdown" - ) + // Don't trigger the goals if the buffer is not owned by us + if (languages.match(coqLSPDocumentSelector, textEditor.document) < 1) return; const kind = diff --git a/editor/code/src/config.ts b/editor/code/src/config.ts index 73147263..2cfb0b57 100644 --- a/editor/code/src/config.ts +++ b/editor/code/src/config.ts @@ -1,4 +1,4 @@ -import { ExtensionContext, workspace } from "vscode"; +import { DocumentSelector, ExtensionContext, workspace } from "vscode"; export interface CoqLspServerConfig { client_version: string; @@ -54,3 +54,7 @@ export namespace CoqLspClientConfig { return obj; } } +export const coqLSPDocumentSelector: DocumentSelector = [ + { language: "coq" }, + { language: "markdown", pattern: "**/*.mv" }, +]; diff --git a/editor/code/src/progress.ts b/editor/code/src/progress.ts index 3c058b92..05ad57d2 100644 --- a/editor/code/src/progress.ts +++ b/editor/code/src/progress.ts @@ -1,10 +1,17 @@ import { throttle } from "throttle-debounce"; -import { Disposable, Range, window, OverviewRulerLane } from "vscode"; +import { + Disposable, + Range, + window, + OverviewRulerLane, + languages, +} from "vscode"; import { NotificationType, VersionedTextDocumentIdentifier, } from "vscode-languageclient"; import { BaseLanguageClient } from "vscode-languageclient"; +import { coqLSPDocumentSelector } from "./config"; enum CoqFileProgressKind { Processing = 1, @@ -64,10 +71,7 @@ export class FileProgressManager { }); private cleanDecos() { for (const editor of window.visibleTextEditors) { - if ( - editor.document.languageId === "coq" || - editor.document.languageId === "markdown" - ) { + if (languages.match(coqLSPDocumentSelector, editor.document) > 0) { editor.setDecorations(progressDecoration, []); } }