Merge pull request #887 from coq-community/manual-goal-view-display

feat: Disable the auto display for the proof view

Author: rtetley

client/package.json

@@ -121,6 +121,12 @@
         "title": "Goal and Info view panel",
         "type": "object",
         "properties": {
+          "vscoq.goals.auto": {
+            "scope": "window",
+            "type": "boolean",
+            "default": "true",
+            "description": "Should the goal view automatically display when navigating a coq document."
+          },
           "vscoq.goals.display": {
             "scope": "window",
             "type": "string",
@@ -338,6 +344,12 @@
         "category": "Coq",
         "icon": "$(arrow-up)"
       },
+      {
+        "command": "extension.coq.displayProofView",
+        "title": "Display Proof View",
+        "category": "Coq",
+        "icon": "$(open-preview)"
+      },
       {
         "command": "extension.coq.documentState",
         "title": "Troubleshooting: Get current document state",
@@ -391,6 +403,11 @@
           "command": "extension.coq.reset",
           "group": "navigation@5"
         },
+        {
+          "when": "resourceLangId == coq && !config.vscoq.goals.auto",
+          "command": "extension.coq.displayProofView",
+          "group": "navigation@0"
+        },
         {
           "when": "resourceLangId == coq",
           "submenu": "vscoq.menu",

client/src/extension.ts

@@ -1,6 +1,5 @@
 import {workspace, window, commands, languages, ExtensionContext, env,
   TextEditorSelectionChangeEvent,
-  TextEditorSelectionChangeKind,
   TextEditor,
   ViewColumn,
   TextEditorRevealType,
@@ -10,7 +9,6 @@ import {workspace, window, commands, languages, ExtensionContext, env,
   extensions,
   StatusBarAlignment,
   MarkdownString,
-  TextEdit,
   WorkspaceEdit
 } from 'vscode';
 
@@ -251,6 +249,10 @@ export function activate(context: ExtensionContext) {
         registerVscoqTextCommand('showManual', () => {
             commands.executeCommand('simpleBrowser.show', 'https://coq.inria.fr/doc/master/refman/index.html'); 
         });
+        registerVscoqTextCommand('displayProofView', () => {
+            const editor = window.activeTextEditor ? window.activeTextEditor : window.visibleTextEditors[0];
+            GoalPanel.displayProofView(context.extensionUri, editor);
+        });
 
         client.onNotification("vscoq/updateHighlights", (notification) => {
 
@@ -284,7 +286,8 @@ export function activate(context: ExtensionContext) {
 
         client.onNotification("vscoq/proofView", (proofView: ProofViewNotification) => {
             const editor = window.activeTextEditor ? window.activeTextEditor : window.visibleTextEditors[0];
-            GoalPanel.proofViewNotification(context.extensionUri, editor, proofView);
+            const autoDisplay = workspace.getConfiguration('vscoq.goals').auto;
+            GoalPanel.proofViewNotification(context.extensionUri, editor, proofView, autoDisplay);
         });
 
         client.onNotification("vscoq/blockOnError", (notification: ErrorAlertNotification) => {

client/src/panels/GoalPanel.ts

@@ -21,6 +21,7 @@ import Client from "../client";
 export default class GoalPanel {
 
   public static currentPanel: GoalPanel | undefined;
+  public static currentPv: ProofViewNotification | undefined;
   private readonly _panel: WebviewPanel;
   private _disposables: Disposable[] = [];
 
@@ -151,15 +152,22 @@ export default class GoalPanel {
   // Create the goal panel if it doesn't exit and then 
   // handle a proofview notification
   // /////////////////////////////////////////////////////////////////////////////
-  public static proofViewNotification(extensionUri: Uri, editor: TextEditor, pv: ProofViewNotification) {
+  public static proofViewNotification(extensionUri: Uri, editor: TextEditor, pv: ProofViewNotification, autoDisplay: boolean) {
 
     Client.writeToVscoq2Channel("[GoalPanel] Received proofview notification");
 
     if(!GoalPanel.currentPanel) {
-        GoalPanel.render(editor, extensionUri, (goalPanel) => {
-            Client.writeToVscoq2Channel("[GoalPanel] Created new goal panel");
-            goalPanel._handleProofViewResponseOrNotification(pv);
-        });
+        //If autoDisplay is set then render the proofview immediately
+        if(autoDisplay) {
+            GoalPanel.render(editor, extensionUri, (goalPanel) => {
+                Client.writeToVscoq2Channel("[GoalPanel] Created new goal panel");
+                goalPanel._handleProofViewResponseOrNotification(pv);
+            });
+        }
+        //Otherwise record the current proofview notification to render on user prompt
+        else {
+            GoalPanel.currentPv = pv;
+        }
     }
     else {
         Client.writeToVscoq2Channel("[GoalPanel] Rendered in current panel");
@@ -168,6 +176,12 @@ export default class GoalPanel {
 
   }
 
+  public static displayProofView(extensionUri: Uri, editor: TextEditor) {
+    if(GoalPanel.currentPv) {
+        GoalPanel.proofViewNotification(extensionUri, editor, GoalPanel.currentPv, true);
+    }
+  }
+
   private _reset() {
     this._panel.webview.postMessage({ "command": "reset"});
   };