[code] Don't trigger goals buffer action in general Markdown documents

cc: #598
ejgallego · Nov 26, 2023 · 67b8e6c · 67b8e6c
1 parent 9a96682
commit 67b8e6c
Showing 1 changed file with 9 additions and 4 deletions.
diff --git 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 {
@@ -204,14 +206,17 @@ export function activateCoqLSP(
     infoPanel.updateFromServer(client, uri, version, position);
   };
 
+  const coqLSPDocumentSelector : DocumentSelector = [
+    { language: 'coq'},
+    { language: 'markdown', pattern: '**/*.mv' }
+  ];
+
   const goalsCall = (
     textEditor: TextEditor,
     callKind: TextEditorSelectionChangeKind | undefined
   ) => {
-    if (
-      textEditor.document.languageId != "coq" &&
-      textEditor.document.languageId != "markdown"
-    )
+
+    if (languages.match(coqLSPDocumentSelector, textEditor.document) < 1)
       return;
 
     const kind =