[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 16, 2023 · b998bbc · b998bbc
1 parent c008185
commit b998bbc
Show file tree

Hide file tree

Showing 5 changed files with 40 additions and 9 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -42,6 +42,9 @@
  - New `pretac` field for preprocessing of goals with a tactic using
    speculative execution, this is experimental for now (@amblafont,
    @ejgallego, #573, helps with #558)
+ - 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/README.md b/README.md
@@ -65,7 +65,7 @@ and web native usage, providing quite a few extra features from vanilla Coq.
   - [📂 Working With Multiple Files](#-working-with-multiple-files)
 - [📔 Planned Features](#-planned-features)
 - [📕 Protocol Documentation](#-protocol-documentation)
-- [🤸 Contributing](#-contributing)
+- [🤸 Contributing and Extending the System](#-contributing-and-extending-the-system)
 - [🥷 Team](#-team)
   - [🕰️ Past Contributors](#️-past-contributors)
 - [©️ Licensing Information](#️-licensing-information)
@@ -368,7 +368,7 @@ plus some extensions specific to Coq.
 
 Check [the `coq-lsp` protocol documentation](etc/doc/PROTOCOL.md) for more details.
 
-## 🤸 Contributing
+## 🤸 Contributing and Extending the System
 
 Contributions are very welcome! Feel free to chat with the dev team in
 [Zulip](https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp) for any
@@ -381,6 +381,10 @@ Here is a [list of project ideas](etc/ContributionIdeas.md) that could be of
 help in case you are looking for contribution ideas, tho we are convinced that
 the best ideas will arise from using `coq-lsp` in your own Coq projects.
 
+Both Flèche and `coq-lsp` have a preliminary _plugin system_. The VSCode
+extension also exports and API so other extensions use its functionality
+to query and interact with Coq documents.
+
 ## 🥷 Team
 
 - Ali Caglayan (co-coordinator)

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) {
@@ -317,7 +329,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,