more explicit message type: allows body to become empty;

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

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