# HG changeset patch
# User wenzelm
# Date 1482404122 -3600
# Node ID fb42c780d903ffc8c6d0afa8e2f58962a06a7fa5
# Parent  6209e0f7a4e8c104d856662b5a44582ec16098ca
proper clean_yxml;

diff -r 6209e0f7a4e8 -r fb42c780d903 src/Tools/VSCode/src/channel.scala
--- 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)