diff --git a/src/workspace-element.js b/src/workspace-element.js index bd0e1b971..188795f9b 100644 --- a/src/workspace-element.js +++ b/src/workspace-element.js @@ -132,6 +132,10 @@ class WorkspaceElement extends HTMLElement { return this } + destroy () { + this.subscriptions.dispose() + } + getModel () { return this.model } handleDragStart (event) { diff --git a/src/workspace.js b/src/workspace.js index 127168748..66e7f8ba5 100644 --- a/src/workspace.js +++ b/src/workspace.js @@ -310,7 +310,10 @@ module.exports = class Workspace extends Model { this.originalFontSize = null this.openers = [] this.destroyedItemURIs = [] - this.element = null + if (this.element) { + this.element.destroy() + this.element = null + } this.consumeServices(this.packageManager) } @@ -1570,6 +1573,7 @@ module.exports = class Workspace extends Model { if (this.activeItemSubscriptions != null) { this.activeItemSubscriptions.dispose() } + if (this.element) this.element.destroy() } /*