src/Tools/VSCode/src/protocol.scala
changeset 66090 5e1c1b366ac3
parent 66062 175772371cd0
child 66096 6187612e83c1
--- a/src/Tools/VSCode/src/protocol.scala	Tue Jun 13 22:39:57 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Wed Jun 14 11:32:47 2017 +0200
@@ -462,8 +462,8 @@
 
   object Dynamic_Output
   {
-    def apply(body: String): JSON.T =
-      Notification("PIDE/dynamic_output", Map("content" -> body))
+    def apply(content: String): JSON.T =
+      Notification("PIDE/dynamic_output", Map("content" -> content))
   }