--- a/src/Tools/VSCode/src/channel.scala Thu Dec 22 11:38:16 2016 +0100
+++ b/src/Tools/VSCode/src/channel.scala Thu Dec 22 11:55:22 2016 +0100
@@ -91,7 +91,7 @@
/* display message */
def display_message(message_type: Int, message: String, show: Boolean = true): Unit =
- write(Protocol.DisplayMessage(message_type, message, show))
+ write(Protocol.DisplayMessage(message_type, Output.clean_yxml(message), show))
def error_message(message: String, show: Boolean = true): Unit =
display_message(Protocol.MessageType.Error, message, show)