Merge pull request #116 from ejgallego/goals_click

[goals] Show goals on click (+ configuration options).
ejgallego · Dec 26, 2022 · 7620f83 · 7620f83
2 parents c5d0694 + 40e4f6b
commit 7620f83
Show file tree

Hide file tree

Showing 4 changed files with 57 additions and 10 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -16,6 +16,9 @@
  - 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 to follow cursor in different ways (@ejgallego, #116,
+   fixes #89)
 
 # coq-lsp 0.1.0: Memory
 -----------------------

diff --git a/editor/code/package.json b/editor/code/package.json
@@ -123,6 +123,13 @@
             "type": "boolean",
             "default": false,
             "description": "Show Coq's Info messages as diagnostics, such as 'foo has been defined.' and miscellaneous operational messages."
+          },
+          "coq-lsp.show_goals_on": {
+            "type": "number",
+            "default": 1,
+            "description": "When to show goals and information about the current cursor",
+            "enum": [0,1,2],
+            "enumItemLabels": ["Don't follow cursor", "Show on click", "Show on click and on cursor movement"]
           }
         }
       }

diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts
@@ -7,7 +7,8 @@ import {
     ViewColumn,
     Uri,
     TextEditor,
-    OverviewRulerLane
+    OverviewRulerLane,
+    WorkspaceConfiguration
 } from "vscode";
 import * as vscode from "vscode";
 import { Range } from "vscode-languageclient";
@@ -19,6 +20,21 @@ import {
 import { GoalPanel } from "./goals";
 import { coqFileProgress, CoqFileProgressParams } from "./progress";
 
+enum ShowGoalsOnCursorChange {
+    Never = 0,
+    OnMouse = 1,
+    OnMouseAndKeyboard = 2
+};
+
+interface CoqLspConfig {
+    eager_diagnostics: boolean,
+    ok_diagnostics: boolean,
+    goal_after_tactic: boolean,
+    show_coq_info_messages: boolean,
+    show_goals_on : ShowGoalsOnCursorChange
+}
+
+let config : CoqLspConfig;
 let client: LanguageClient;
 let goalPanel: GoalPanel | null;
 
@@ -52,19 +68,22 @@ export function activate(context: ExtensionContext): void {
 
         window.showInformationMessage("Coq Language Server: starting");
 
-        const config = workspace.getConfiguration("coq-lsp");
-        const initializationOptions = {
-            eager_diagnostics: config.eager_diagnostics,
-            ok_diagnostics: config.ok_diagnostics,
+        const wsConfig = workspace.getConfiguration("coq-lsp");
+        config = {
+            eager_diagnostics: wsConfig.eager_diagnostics,
+            ok_diagnostics: wsConfig.ok_diagnostics,
+            goal_after_tactic: wsConfig.goal_after_tactic,
+            show_coq_info_messages: wsConfig.show_coq_info_messages,
+            show_goals_on: wsConfig.show_goals_on
         };
 
         const clientOptions: LanguageClientOptions = {
             documentSelector: [{ scheme: "file", language: "coq" }],
             outputChannelName: "Coq LSP Server Events",
             revealOutputChannelOn: RevealOutputChannelOn.Info,
-            initializationOptions,
+            initializationOptions: config,
         };
-        const serverOptions = { command: config.path, args: config.args };
+        const serverOptions = { command: wsConfig.path, args: wsConfig.args };
 
         client = new LanguageClient(
             "coq-lsp-server",
@@ -83,6 +102,7 @@ export function activate(context: ExtensionContext): void {
         // XXX: Fix this mess with the lifetime of the panel
         goalPanel = panelFactory(context);
     };
+
     const progressDecoration = window.createTextEditorDecorationType(
         { overviewRulerColor: 'rgba(255,165,0,0.5)', overviewRulerLane: OverviewRulerLane.Left}
     );
@@ -114,6 +134,20 @@ export function activate(context: ExtensionContext): void {
         }
     };
 
+    let disposable = window.onDidChangeTextEditorSelection((evt : vscode.TextEditorSelectionChangeEvent) => {
+        const show =
+            (evt.kind == vscode.TextEditorSelectionChangeKind.Keyboard && 
+             config.show_goals_on == ShowGoalsOnCursorChange.OnMouseAndKeyboard) ||
+            (evt.kind == vscode.TextEditorSelectionChangeKind.Mouse &&
+             (config.show_goals_on == ShowGoalsOnCursorChange.OnMouse ||
+              config.show_goals_on == ShowGoalsOnCursorChange.OnMouseAndKeyboard));
+
+        if(show) {
+            goals(evt.textEditor);
+        }});
+
+    context.subscriptions.push(disposable);
+
     coqCommand("restart", restart);
     coqEditorCommand("goals", goals);
 

diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts
@@ -1,5 +1,5 @@
 import { Webview, Position, Uri, WebviewPanel } from "vscode";
-import { RequestType } from "vscode-languageclient";
+import { RequestType, TextDocumentIdentifier, VersionedTextDocumentIdentifier } from "vscode-languageclient";
 import { LanguageClient } from "vscode-languageclient/node";
 
 interface Hyp {
@@ -11,7 +11,10 @@ interface Goal {
     hyps: Hyp[];
 }
 
-interface GoalRequest {}
+interface GoalRequest {
+    textDocument: TextDocumentIdentifier,
+    position: Position
+}
 
 // returns the HTML code of goals environment
 function getGoalsEnvContent(goals: Goal[]) {
@@ -88,7 +91,7 @@ class GoalView {
     // LSP Protocol extension for Goals
     sendGoalsRequest(uri: Uri, position: Position) {
         let doc = { uri: uri.toString() };
-        let cursor = { textDocument: doc, position: position };
+        let cursor : GoalRequest = { textDocument: doc, position: position };
         const req = new RequestType<GoalRequest, Goal[], void>("proof/goals");
         this.client.sendRequest(req, cursor).then(
             (goals) => this.display(goals),