Merge pull request #625 from ejgallego/stricter_goals_focus

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

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
 -------------------------------

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 =

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" },
+];

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, []);
       }
     }