# HG changeset patch
# User wenzelm
# Date 1489338306 -3600
# Node ID 1227a68fac7ac178ef02c9697bda5ee09578036b
# Parent  6bd7081f831962718d1bbf544b0fac3ec95223f3
more explicit message type: allows body to become empty;

diff -r 6bd7081f8319 -r 1227a68fac7a src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Sun Mar 12 17:59:03 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sun Mar 12 18:05:06 2017 +0100
@@ -34,9 +34,16 @@
 }
 
 const caret_update_type = new NotificationType<Caret_Update, void>("PIDE/caret_update")
-const dynamic_output_type = new NotificationType<string, void>("PIDE/dynamic_output")
+let last_caret_update: Caret_Update = {}
+
 
-let last_caret_update: Caret_Update = {}
+interface Dynamic_Output
+{
+  body: string
+}
+
+const dynamic_output_type = new NotificationType<Dynamic_Output, void>("PIDE/dynamic_output")
+
 
 
 /* activate extension */
@@ -99,12 +106,7 @@
     client.onReady().then(() =>
     {
       client.onNotification(dynamic_output_type,
-        body => {
-          if (body) {
-            dynamic_output.clear()
-            dynamic_output.appendLine(body)
-          }
-        })
+        params => { dynamic_output.clear(); dynamic_output.appendLine(params.body) })
       vscode.window.onDidChangeActiveTextEditor(_ => update_caret())
       vscode.window.onDidChangeTextEditorSelection(_ => update_caret())
       update_caret()
diff -r 6bd7081f8319 -r 1227a68fac7a src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Sun Mar 12 17:59:03 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Sun Mar 12 18:05:06 2017 +0100
@@ -443,6 +443,6 @@
   object Dynamic_Output
   {
     def apply(body: String): JSON.T =
-      Notification("PIDE/dynamic_output", body)
+      Notification("PIDE/dynamic_output", Map("body" -> body))
   }
 }