feat: send notifications from infoview

leanprover · Jul 13, 2021 · 6e188d6 · 6e188d6
1 parent 8010e34
commit 6e188d6
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/lean4-infoview/src/infoviewApi.ts b/lean4-infoview/src/infoviewApi.ts
@@ -18,6 +18,8 @@ export interface EditorApi {
 
   /** Make a request to the LSP server. */
   sendClientRequest(method: string, params: any): Promise<any>;
+  /** Send a notification to the LSP server. */
+  sendClientNotification(method: string, params: any): Promise<void>;
 
   /**
    * Subscribe to notifications from the LSP server with the specified `method`.

diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts
@@ -25,8 +25,11 @@ export class InfoProvider implements Disposable {
     private clientNotifSubscriptions: Map<string, [number, Disposable]> = new Map();
 
     private editorApi : EditorApi = {
-        sendClientRequest: async <T extends TextDocumentIdentifier, U>(method: string, req: T): Promise<U> => {
-            return await this.client.client.sendRequest(method, req);
+        sendClientRequest: async (method: string, params: any): Promise<any> => {
+            return this.client.client.sendRequest(method, params);
+        },
+        sendClientNotification: async (method: string, params: any): Promise<void> => {
+            void this.client.client.sendNotification(method, params);
         },
         subscribeServerNotifications: async (method) => {
             const el = this.serverNotifSubscriptions.get(method);