[client] [vscode] Export Query Goals API

This way other extensions can implement their own commands that query Coq goals With #574, close #558 Co-authored-by: Ambroise Lafont <[email protected]>
ejgallego · Oct 13, 2023 · 4e66680 · 4e66680
1 parent b4c3d52
commit 4e66680
Show file tree

Hide file tree

Showing 4 changed files with 34 additions and 7 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -39,6 +39,9 @@
  - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
    @CohenCyril, #572, via
    https://github.com/coq-community/coq-nix-toolbox/pull/164 )
+ - Export Query Goals API in VSCode client; this way other extensions
+   can implement their own commands that query Coq goals (@amblafont,
+   @ejgallego, #576, closes #558)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------

diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts
@@ -25,9 +25,12 @@ import {
   FlecheDocumentParams,
   FlecheDocument,
   FlecheSaveParams,
+  GoalRequest,
+  GoalAnswer,
+  PpString,
 } from "../lib/types";
 import { CoqLspClientConfig, CoqLspServerConfig } from "./config";
-import { InfoPanel } from "./goals";
+import { InfoPanel, goalReq } from "./goals";
 import { FileProgressManager } from "./progress";
 import { coqPerfData, PerfDataView } from "./perf";
 
@@ -54,10 +57,19 @@ export type ClientFactoryType = (
   wsConfig: WorkspaceConfiguration
 ) => BaseLanguageClient;
 
+// Extension API type (note this doesn't live in `lib` as this is VSCode specific)
+export interface CoqLspAPI {
+  /**
+   * Query goals from Coq
+   * @param params goal request parameters
+   */
+  goalsRequest(params: GoalRequest): Promise<GoalAnswer<PpString>>;
+}
+
 export function activateCoqLSP(
   context: ExtensionContext,
   clientFactory: ClientFactoryType
-): void {
+): CoqLspAPI {
   window.showInformationMessage("Coq LSP Extension: Going to activate!");
 
   function coqCommand(command: string, fn: () => void) {
@@ -315,7 +327,14 @@ export function activateCoqLSP(
   createEnableButton();
 
   start();
+
+  return {
+    goalsRequest: (params) => {
+      return client.sendRequest(goalReq, params);
+    },
+  };
 }
+
 export function deactivateCoqLSP(): Thenable<void> | undefined {
   if (!client) {
     return undefined;

diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts
@@ -14,7 +14,7 @@ import {
 } from "vscode-languageclient";
 import { GoalRequest, GoalAnswer, PpString } from "../lib/types";
 
-const infoReq = new RequestType<GoalRequest, GoalAnswer<PpString>, void>(
+export const goalReq = new RequestType<GoalRequest, GoalAnswer<PpString>, void>(
   "proof/goals"
 );
 
@@ -101,7 +101,7 @@ export class InfoPanel {
   // LSP Protocol extension for Goals
   sendGoalsRequest(client: BaseLanguageClient, params: GoalRequest) {
     this.requestSent(params);
-    client.sendRequest(infoReq, params).then(
+    client.sendRequest(goalReq, params).then(
       (goals) => this.requestDisplay(goals),
       (reason) => this.requestError(reason)
     );
@@ -110,7 +110,7 @@ export class InfoPanel {
   sendVizxRequest(client: BaseLanguageClient, params: GoalRequest) {
     this.requestSent(params);
     console.log(params.pp_format);
-    client.sendRequest(infoReq, params).then(
+    client.sendRequest(goalReq, params).then(
       (goals) => this.requestVizxDisplay(goals),
       (reason) => this.requestError(reason)
     );

diff --git a/editor/code/src/node.ts b/editor/code/src/node.ts
@@ -1,8 +1,13 @@
 import { ExtensionContext } from "vscode";
 import { LanguageClient, ServerOptions } from "vscode-languageclient/node";
-import { activateCoqLSP, ClientFactoryType, deactivateCoqLSP } from "./client";
+import {
+  activateCoqLSP,
+  ClientFactoryType,
+  CoqLspAPI,
+  deactivateCoqLSP,
+} from "./client";
 
-export function activate(context: ExtensionContext): void {
+export function activate(context: ExtensionContext): CoqLspAPI {
   const cf: ClientFactoryType = (context, clientOptions, wsConfig) => {
     const serverOptions: ServerOptions = {
       command: wsConfig.path,