From 67b8e6c1892490e9267310b28daa1eb62b888073 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sun, 26 Nov 2023 19:57:50 +0100
Subject: [PATCH] [code] Don't trigger goals buffer action in general Markdown
 documents

cc: #598
---
 editor/code/src/client.ts | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts
index 313e777b1..712f8de70 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 {
@@ -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 =