--- 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)