Skip to content

Commit

Permalink
fix: register event listeners for proper disposal of client provider (#…
Browse files Browse the repository at this point in the history
…498)

This adds the disposable returned by the event registrations to
`this.subscriptions` so that calling `dispose` will get rid of all event
listeners.

This will help with lean4web, but is probably generally the right thing
to do here.
  • Loading branch information
abentkamp authored Nov 20, 2024
1 parent 24f2edd commit e2132c6
Showing 1 changed file with 17 additions and 15 deletions.
32 changes: 17 additions & 15 deletions vscode-lean4/src/utils/clientProvider.ts
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,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(
Expand All @@ -79,24 +79,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 {
Expand Down

0 comments on commit e2132c6

Please sign in to comment.