[goals] Show goals on click (+ configuration options).

We allow to show goals on click, on cursor movement, or on both. User-configurable. Fixes #89
ejgallego · Dec 26, 2022 · 23ac43e · 23ac43e
1 parent c5d0694
commit 23ac43e
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 0 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -16,6 +16,8 @@
  - Send `$/coq/fileProgress` progress notifications from server,
    similarly to what Lean does; display them in Code's right gutter
    (@ejgallego, #106, fixes #54)
+ - Show goals on click by default, allow users to configure the behavior
+   (@ejgallego, #116, fixes #89)
 
 # coq-lsp 0.1.0: Memory
 -----------------------

diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts
@@ -82,7 +82,14 @@ export function activate(context: ExtensionContext): void {
 
         // XXX: Fix this mess with the lifetime of the panel
         goalPanel = panelFactory(context);
+
+        context.subscriptions.push(window.onDidChangeTextEditorSelection((evt : vscode.TextEditorSelectionChangeEvent) => {
+            if(evt.kind == vscode.TextEditorSelectionChangeKind.Mouse) {
+                goals(evt.textEditor);
+            }
+        }));
     };
+
     const progressDecoration = window.createTextEditorDecorationType(
         { overviewRulerColor: 'rgba(255,165,0,0.5)', overviewRulerLane: OverviewRulerLane.Left}
     );