# HG changeset patch
# User wenzelm
# Date 1496174977 -7200
# Node ID 5754708a2d05fe9d0b72f7953c371780c2930837
# Parent  c51b74be23b6514ecb7c8f521cc2281cc4448978
tuned;

diff -r c51b74be23b6 -r 5754708a2d05 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Tue May 30 22:06:39 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Tue May 30 22:09:37 2017 +0200
@@ -56,12 +56,7 @@
       client.onNotification(protocol.decoration_type, decorations.apply_decoration))
 
 
-    /* caret handling and dynamic output */
-
-    const dynamic_output = window.createOutputChannel("Isabelle Output")
-    context.subscriptions.push(dynamic_output)
-    dynamic_output.show(true)
-    dynamic_output.hide()
+    /* caret handling */
 
     function update_caret()
     {
@@ -82,8 +77,6 @@
 
     client.onReady().then(() =>
     {
-      client.onNotification(protocol.dynamic_output_type,
-        params => { dynamic_output.clear(); dynamic_output.appendLine(params.body) })
       context.subscriptions.push(
         window.onDidChangeActiveTextEditor(_ => update_caret()),
         window.onDidChangeTextEditorSelection(_ => update_caret()))
@@ -91,6 +84,20 @@
     })
 
 
+    /* dynamic output */
+
+    const dynamic_output = window.createOutputChannel("Isabelle Output")
+    context.subscriptions.push(dynamic_output)
+    dynamic_output.show(true)
+    dynamic_output.hide()
+
+    client.onReady().then(() =>
+    {
+      client.onNotification(protocol.dynamic_output_type,
+        params => { dynamic_output.clear(); dynamic_output.appendLine(params.body) })
+    })
+
+
     /* dynamic preview */
 
     preview.init(context)