diff --git a/lean4-infoview/src/infoviewApi.ts b/lean4-infoview/src/infoviewApi.ts index a19d53ca8..23f2a8c3b 100644 --- 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; + /** Send a notification to the LSP server. */ + sendClientNotification(method: string, params: any): Promise; /** * 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 index fe037287d..4bddc403b 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -25,8 +25,11 @@ export class InfoProvider implements Disposable { private clientNotifSubscriptions: Map = new Map(); private editorApi : EditorApi = { - sendClientRequest: async (method: string, req: T): Promise => { - return await this.client.client.sendRequest(method, req); + sendClientRequest: async (method: string, params: any): Promise => { + return this.client.client.sendRequest(method, params); + }, + sendClientNotification: async (method: string, params: any): Promise => { + void this.client.client.sendNotification(method, params); }, subscribeServerNotifications: async (method) => { const el = this.serverNotifSubscriptions.get(method);