--- a/src/Tools/VSCode/src/channel.scala Wed Apr 07 18:05:14 2021 +0200
+++ b/src/Tools/VSCode/src/channel.scala Wed Apr 07 18:05:48 2021 +0200
@@ -79,7 +79,7 @@
/* display message */
- def display_message(message_type: Int, msg: String, show: Boolean = true): Unit =
+ def display_message(message_type: Int, msg: String, show: Boolean): Unit =
write(LSP.DisplayMessage(message_type, Output.clean_yxml(msg), show))
def error_message(msg: String): Unit = display_message(LSP.MessageType.Error, msg, true)