fix: register event listeners for proper disposal of client provider

leanprover · Jul 7, 2024 · eb181a0 · eb181a0
1 parent b153d53
commit eb181a0
Showing 1 changed file with 17 additions and 15 deletions.
diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts
@@ -58,7 +58,7 @@ export class LeanClientProvider implements Disposable {
  this.installer = installer
 
  // we must setup the installChanged event handler first before any didOpenEditor calls.
- installer.installChanged(async (uri: FileUri) => await this.onInstallChanged(uri))
+ this.subscriptions.push(installer.installChanged(async (uri: FileUri) => await this.onInstallChanged(uri)))
 
  window.visibleTextEditors.forEach(e => this.didOpenEditor(e.document))
  this.subscriptions.push(
@@ -77,24 +77,26 @@ export class LeanClientProvider implements Disposable {
  commands.registerCommand('lean4.stopServer', () => this.stopActiveClient()),
  )
 
- workspace.onDidOpenTextDocument(document => this.didOpenEditor(document))
+ this.subscriptions.push(workspace.onDidOpenTextDocument(document => this.didOpenEditor(document)))
 
- workspace.onDidChangeWorkspaceFolders(event => {
- // Remove all clients that are not referenced by any folder anymore
- if (event.removed.length === 0) {
- return
- }
- this.clients.forEach((client, key) => {
- if (client.folderUri.scheme === 'untitled' || getWorkspaceFolderUri(client.folderUri)) {
+ this.subscriptions.push(
+ workspace.onDidChangeWorkspaceFolders(event => {
+ // Remove all clients that are not referenced by any folder anymore
+ if (event.removed.length === 0) {
  return
  }
+ this.clients.forEach((client, key) => {
+ if (client.folderUri.scheme === 'untitled' || getWorkspaceFolderUri(client.folderUri)) {
+ return
+ }
 
- logger.log(`[ClientProvider] onDidChangeWorkspaceFolders removing client for ${key}`)
- this.clients.delete(key)
- client.dispose()
- this.clientRemovedEmitter.fire(client)
- })
- })
+ logger.log(`[ClientProvider] onDidChangeWorkspaceFolders removing client for ${key}`)
+ this.clients.delete(key)
+ client.dispose()
+ this.clientRemovedEmitter.fire(client)
+ })
+ }),
+ )
  }
 
  getActiveClient(): LeanClient | undefined {