From 45c36167e01cd8f40df2ec342d2f5df7f5b2432a Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Tue, 10 Dec 2024 11:44:43 +0100 Subject: [PATCH] fix: dispose webviewPanel in InfoProvider.dispose (#514) The InfoProvider opens the webviewPanel, so it should also call the webviewPanel's dispose function when gettting disposed. --- vscode-lean4/src/infoview.ts | 1 + 1 file changed, 1 insertion(+) diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index 38e4dea1..3412ced8 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -481,6 +481,7 @@ export class InfoProvider implements Disposable { // active client is changing. this.clearNotificationHandlers() this.clearRpcSessions(null) + this.webviewPanel?.dispose() for (const s of this.clientSubscriptions) { s.dispose() }