# HG changeset patch
# User wenzelm
# Date 1617811548 -7200
# Node ID 1240abf2e3f5143ce1356153fc28496794dfb8c5
# Parent  a69197959ab6bd7d87b1c887d766bde4166d5668
tuned signature;

diff -r a69197959ab6 -r 1240abf2e3f5 src/Tools/VSCode/src/channel.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)
diff -r a69197959ab6 -r 1240abf2e3f5 src/Tools/VSCode/src/lsp.scala
--- 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))
   }