[vscode] Provide generic user goal request hook.

This allows extensions to register without having to modify ours; it
should subsume previous hooks for `VIXZ` and `VIZCAR` visualizers.

There are many more improvements we can do to this API.

Fixes #538

CHANGES.md

@@ -78,6 +78,9 @@
  - The `coq-lsp.pp_type` VSCode client option now takes effect
    immediately, no more need to restart the server to get different
    goal display formats (@ejgallego, #675)
+ - new public VSCode extension API so other extensions can perform
+   actions when the user request the goals (@ejgallego, @bhaktishh,
+   #672, fixes #538)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

editor/code/src/client.ts

@@ -68,9 +68,13 @@ export type ClientFactoryType = (
 export interface CoqLspAPI {
   /**
    * Query goals from Coq
-   * @param params goal request parameters
    */
   goalsRequest(params: GoalRequest): Promise<GoalAnswer<PpString>>;
+
+  /**
+   * Register callback on user-initiated goals request
+   */
+  onUserGoals(fn: (goals: GoalAnswer<String>) => void): Disposable;
 }
 
 export function activateCoqLSP(
@@ -363,6 +367,10 @@ export function activateCoqLSP(
     goalsRequest: (params) => {
       return client.sendRequest(goalReq, params);
     },
+    onUserGoals: (fn) => {
+      infoPanel.registerObserver(fn);
+      return new Disposable(() => infoPanel.unregisterObserver(fn));
+    },
   };
 }
 

editor/code/src/goals.ts

@@ -6,6 +6,7 @@ import {
   ViewColumn,
   extensions,
   commands,
+  TextDocument,
 } from "vscode";
 import {
   BaseLanguageClient,
@@ -21,6 +22,7 @@ export const goalReq = new RequestType<GoalRequest, GoalAnswer<PpString>, void>(
 export class InfoPanel {
   private panel: WebviewPanel | null = null;
   private extensionUri: Uri;
+  private listeners: Array<(goals: GoalAnswer<String>) => void> = [];
 
   constructor(extensionUri: Uri) {
     this.extensionUri = extensionUri;
@@ -31,6 +33,17 @@ export class InfoPanel {
     this.panel?.dispose();
   }
 
+  registerObserver(fn: (goals: GoalAnswer<String>) => void) {
+    this.listeners.push(fn);
+  }
+
+  unregisterObserver(fn: (goals: GoalAnswer<String>) => void) {
+    let index = this.listeners.indexOf(fn);
+    if (index >= 0) {
+      this.listeners.splice(index, 1);
+    }
+  }
+
   panelFactory() {
     let webviewOpts = { enableScripts: true, enableFindWidget: true };
     this.panel = window.createWebviewPanel(
@@ -88,48 +101,33 @@ export class InfoPanel {
     this.postMessage("renderGoals", goals);
   }
 
-  requestVizxDisplay(goals: GoalAnswer<PpString>) {
-    console.log(goals);
-    commands.executeCommand("vizx.lspRender", goals);
-  }
-
-  requestVizCarDisplay(goals: GoalAnswer<PpString>) {
-    console.log(goals);
-    commands.executeCommand("vizcar.lspRender", goals);
-  }
-
   // notify the info panel that we found an error
   requestError(e: any) {
     this.postMessage("infoError", e);
   }
 
   // LSP Protocol extension for Goals
-  sendGoalsRequest(client: BaseLanguageClient, params: GoalRequest) {
+  updateInfoPanelForCursor(client: BaseLanguageClient, params: GoalRequest) {
     this.requestSent(params);
     client.sendRequest(goalReq, params).then(
       (goals) => this.requestDisplay(goals),
       (reason) => this.requestError(reason)
     );
   }
 
-  sendVizxRequest(client: BaseLanguageClient, params: GoalRequest) {
-    this.requestSent(params);
-    console.log(params.pp_format);
-    client.sendRequest(goalReq, params).then(
-      (goals) => this.requestVizxDisplay(goals),
-      (reason) => this.requestError(reason)
-    );
-  }
-
-  sendVizCarRequest(client: BaseLanguageClient, params: GoalRequest) {
-    this.requestSent(params);
-    console.log(params.pp_format);
-    client.sendRequest(goalReq, params).then(
-      (goals) => this.requestVizCarDisplay(goals),
-      (reason) => this.requestError(reason)
-    );
+  updateAPIClientForCursor(client: BaseLanguageClient, params: GoalRequest) {
+    if (this.listeners.length > 0) {
+      params.pp_format = "Str";
+      client.sendRequest(goalReq, params).then(
+        (goals) => {
+          let goals_fn = goals as GoalAnswer<String>;
+          this.listeners.forEach((fn) => fn(goals_fn));
+        },
+        // We should actually provide a better setup so we can pass the rejection of the promise to our clients, YMMV tho.
+        (reason) => this.requestError(reason)
+      );
+    }
   }
-
   updateFromServer(
     client: BaseLanguageClient,
     uri: Uri,
@@ -146,23 +144,7 @@ export class InfoPanel {
     // let command = "idtac.";
     // let cursor: GoalRequest = { textDocument, position, command };
     let cursor: GoalRequest = { textDocument, position, pp_format };
-    this.sendGoalsRequest(client, cursor);
-
-    let strCursor: GoalRequest = {
-      textDocument,
-      position,
-      pp_format: "Str",
-    };
-
-    let vizx = extensions.getExtension("inQWIRE.vizx");
-    if (vizx?.isActive) {
-      console.log("vizx active in updateFromServer");
-      this.sendVizxRequest(client, strCursor);
-    }
-    let vizcar = extensions.getExtension("inQWIRE.vizcar");
-    if (vizcar?.isActive) {
-      console.log("vizcar active in updateFromServer");
-      this.sendVizCarRequest(client, strCursor);
-    }
+    this.updateInfoPanelForCursor(client, cursor);
+    this.updateAPIClientForCursor(client, cursor);
   }
 }

etc/doc/PROTOCOL.md

@@ -8,6 +8,9 @@ implements some extensions tailored to improve Coq-specific use.
 As of today, this document is written for the 3.17 version of the LSP specification:
 https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification
 
+For documentation on the API of the VSCode/VSCodium `coq-lsp`
+extension see the [VSCODE_API](./VSCODE_API.md) file instead.
+
 See also the upstream LSP issue on generic support for Proof
 Assistants
 https://github.com/microsoft/language-server-protocol/issues/1414

etc/doc/README.md

@@ -0,0 +1,10 @@
+# Welcome to `coq-lsp` documentation
+
+For now this is just a stub, we will add more information here
+soon. You can find some useful documents here:
+
+- `coq-lsp` core [README](../../README.md)
+- `coq-lsp` [contributing guide](../../CONTRIBUTING.md)
+- `coq-lsp` users manual (upcoming)
+- [`coq-lsp` LSP Protocol Documentation](./PROTOCOL.md)
+- [VSCode client API documentation](./VSCODE_API.md)

etc/doc/VSCODE_API.md

@@ -0,0 +1,35 @@
+# Welcome to the developer documentation for the coq-lsp VSCode extension
+
+As of today, the extension provides two extensions for other
+developers to use:
+
+```typescript
+export interface CoqLspAPI {
+  /**
+   * Query goals from Coq
+   */
+  goalsRequest(params: GoalRequest): Promise<GoalAnswer<PpString>>;
+
+  /**
+   * Register callback action on user-initiated goals request
+   */
+  onUserGoals(fn: (goals: GoalAnswer<String>) => void): Disposable;
+}
+```
+
+Types are for now in the `lib/types.ts` file, we would be happy to
+provide a separate package soon.
+
+## Querying goals from Coq:
+
+Use `goalsRequest` to perform your own queries to Coq, and handle the
+answer in your own extension.
+
+## Reacting to user demands for Goals:
+
+Alternatively, you can instead have `coq-lsp` call your code when the
+user request the goals. In order to register the callback, you can use
+the `onUserGoals` API function.
+
+Don't forget to dispose of your callback when your extension is
+de-activated.