# HG changeset patch
# User wenzelm
# Date 1496165106 -7200
# Node ID f20739a63a44159ac1bef7c4adb7c16f1b0ef2ff
# Parent  fd5f80ee2de080f05254cdea53a31287479a1a10
more careful treatment of context.subscriptions;

diff -r fd5f80ee2de0 -r f20739a63a44 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Tue May 30 19:19:39 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Tue May 30 19:25:06 2017 +0200
@@ -46,10 +46,11 @@
     /* decorations */
 
     decorations.init(context)
-    workspace.onDidChangeConfiguration(() => decorations.init(context))
-    workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document))
-    window.onDidChangeActiveTextEditor(decorations.update_editor)
-    workspace.onDidCloseTextDocument(decorations.close_document)
+    context.subscriptions.push(
+      workspace.onDidChangeConfiguration(() => decorations.init(context)),
+      workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document)),
+      window.onDidChangeActiveTextEditor(decorations.update_editor),
+      workspace.onDidCloseTextDocument(decorations.close_document))
 
     client.onReady().then(() =>
       client.onNotification(protocol.decoration_type, decorations.apply_decoration))
@@ -83,8 +84,9 @@
     {
       client.onNotification(protocol.dynamic_output_type,
         params => { dynamic_output.clear(); dynamic_output.appendLine(params.body) })
-      window.onDidChangeActiveTextEditor(_ => update_caret())
-      window.onDidChangeTextEditorSelection(_ => update_caret())
+      context.subscriptions.push(
+        window.onDidChangeActiveTextEditor(_ => update_caret()),
+        window.onDidChangeTextEditorSelection(_ => update_caret()))
       update_caret()
     })
 
@@ -92,7 +94,8 @@
     /* preview */
 
     preview.init(context)
-    workspace.onDidChangeTextDocument(event => preview.touch_document(event.document))
+    context.subscriptions.push(
+      workspace.onDidChangeTextDocument(event => preview.touch_document(event.document)))
 
 
     /* start server */