tuned signature;
authorwenzelm
Wed, 07 Apr 2021 18:05:48 +0200
changeset 73541 1240abf2e3f5
parent 73540 a69197959ab6
child 73542 e4fde6b3e09a
tuned signature;
src/Tools/VSCode/src/channel.scala
src/Tools/VSCode/src/lsp.scala
--- 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))
   }