Merge pull request #649 from coq-community/vim-compat

Fix compatibility with vim extenion
coq · Oct 3, 2023 · 1a99fd5 · 1a99fd5
2 parents 92eeb56 + ba2a8ab
commit 1a99fd5
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 7 deletions.
diff --git a/client/package.json b/client/package.json
@@ -276,23 +276,27 @@
         "command": "extension.coq.interpretToPoint",
         "category": "Coq",
         "title": "Interpret to point",
-        "description": "Interprets the current coq file until the given point"
+        "description": "Interprets the current coq file until the given point",
+        "enablement": "config.vscoq.proof.mode == 0"
       },
       {
         "command": "extension.coq.interpretToEnd",
         "category": "Coq",
         "title": "Interpret to end",
-        "description": "Interprets the current coq file until the end"
+        "description": "Interprets the current coq file until the end",
+        "enablement": "config.vscoq.proof.mode == 0"
       },
       {
         "command": "extension.coq.stepForward",
         "title": "Step Forward",
-        "category": "Coq"
+        "category": "Coq",
+        "enablement": "config.vscoq.proof.mode == 0"
       },
       {
         "command": "extension.coq.stepBackward",
         "title": "Step Backward",
-        "category": "Coq"
+        "category": "Coq",
+        "enablement": "config.vscoq.proof.mode == 0"
       },
       {
         "command": "extension.coq.documentState",

diff --git a/client/src/extension.ts b/client/src/extension.ts
@@ -237,9 +237,8 @@ export function activate(context: ExtensionContext) {
 
             let goalsHook = window.onDidChangeTextEditorSelection(
                 (evt: TextEditorSelectionChangeEvent) => {                    
-                    if (evt.textEditor.document.languageId === "coq" 
-                        && workspace.getConfiguration('vscoq.proof').mode === 1
-                        && isMouseOrKeyboardEvent(evt)) 
+                    if (evt.textEditor.document.languageId === "coq"
+                        && workspace.getConfiguration('vscoq.proof').mode === 1)
                     {
                         sendInterpretToPoint(evt.textEditor, client);
                     }