Skip to content

Commit

Permalink
[code] Don't trigger goals buffer action in general Markdown documents
Browse files Browse the repository at this point in the history
cc: #598
  • Loading branch information
ejgallego committed Nov 26, 2023
1 parent 9a96682 commit 84ef3d4
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 4 deletions.
2 changes: 2 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
-------------------------------
Expand Down
12 changes: 8 additions & 4 deletions editor/code/src/client.ts
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ import {
ThemeColor,
WorkspaceConfiguration,
Disposable,
DocumentSelector,
languages,
} from "vscode";

import {
Expand Down Expand Up @@ -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 =
Expand Down

0 comments on commit 84ef3d4

Please sign in to comment.