From 943e4e9c34d92a5cfc13781f0db0945cbdf98a25 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
---
 CHANGES.md                |  2 ++
 editor/code/src/client.ts | 12 ++++++++----
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 036dc5396..761b39f97 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, # , 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 313e777b1..506555eb5 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,16 @@ 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 =