# HG changeset patch
# User wenzelm
# Date 1496175240 -7200
# Node ID c208fcf369b7a270c48c3080fd4936fa3ea6de80
# Parent  5754708a2d05fe9d0b72f7953c371780c2930837
tuned -- like Dynamic_Preview;

diff -r 5754708a2d05 -r c208fcf369b7 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Tue May 30 22:09:37 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Tue May 30 22:14:00 2017 +0200
@@ -94,7 +94,7 @@
     client.onReady().then(() =>
     {
       client.onNotification(protocol.dynamic_output_type,
-        params => { dynamic_output.clear(); dynamic_output.appendLine(params.body) })
+        params => { dynamic_output.clear(); dynamic_output.appendLine(params.content) })
     })
 
 
diff -r 5754708a2d05 -r c208fcf369b7 src/Tools/VSCode/extension/src/protocol.ts
--- a/src/Tools/VSCode/extension/src/protocol.ts	Tue May 30 22:09:37 2017 +0200
+++ b/src/Tools/VSCode/extension/src/protocol.ts	Tue May 30 22:14:00 2017 +0200
@@ -39,7 +39,7 @@
 
 export interface Dynamic_Output
 {
-  body: string
+  content: string
 }
 
 export const dynamic_output_type =
diff -r 5754708a2d05 -r c208fcf369b7 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Tue May 30 22:09:37 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Tue May 30 22:14:00 2017 +0200
@@ -461,7 +461,7 @@
   object Dynamic_Output
   {
     def apply(body: String): JSON.T =
-      Notification("PIDE/dynamic_output", Map("body" -> body))
+      Notification("PIDE/dynamic_output", Map("content" -> body))
   }