changeset 65201 | 2d01b30e6ac6 |
parent 65200 | 1227a68fac7a |
child 65229 | cc96b8c3b8cb |
--- a/src/Tools/VSCode/src/protocol.scala Sun Mar 12 18:05:06 2017 +0100 +++ b/src/Tools/VSCode/src/protocol.scala Sun Mar 12 18:45:53 2017 +0100 @@ -422,7 +422,7 @@ } - /* caret handling and dynamic output */ + /* caret handling */ object Caret_Update { @@ -440,6 +440,9 @@ } } + + /* dynamic output */ + object Dynamic_Output { def apply(body: String): JSON.T =