--- 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)
--- a/src/Tools/VSCode/src/lsp.scala Wed Apr 07 18:05:14 2021 +0200
+++ b/src/Tools/VSCode/src/lsp.scala Wed Apr 07 18:05:48 2021 +0200
@@ -259,7 +259,7 @@
object DisplayMessage
{
- def apply(message_type: Int, message: String, show: Boolean = true): JSON.T =
+ def apply(message_type: Int, message: String, show: Boolean): JSON.T =
Notification(if (show) "window/showMessage" else "window/logMessage",
JSON.Object("type" -> message_type, "message" -> message))
}