# HG changeset patch
# User wenzelm
# Date 1482943787 -3600
# Node ID 7888be4fa4962edb844cf436f1a4bf2f69aa86c2
# Parent  0f00e26611648e3d3fb5d2b6787e8520c3831744
clarified signature;

diff -r 0f00e2661164 -r 7888be4fa496 src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Wed Dec 28 17:38:12 2016 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Wed Dec 28 17:49:47 2016 +0100
@@ -90,15 +90,16 @@
 
   /* display message */
 
-  def display_message(message_type: Int, message: String, show: Boolean = true): Unit =
-    write(Protocol.DisplayMessage(message_type, Output.clean_yxml(message), show))
+  def display_message(message_type: Int, msg: String, show: Boolean = true): Unit =
+    write(Protocol.DisplayMessage(message_type, Output.clean_yxml(msg), show))
 
-  def error_message(message: String, show: Boolean = true): Unit =
-    display_message(Protocol.MessageType.Error, message, show)
-  def warning(message: String, show: Boolean = true): Unit =
-    display_message(Protocol.MessageType.Warning, message, show)
-  def writeln(message: String, show: Boolean = true): Unit =
-    display_message(Protocol.MessageType.Info, message, show)
+  def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) }
+  def warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, true) }
+  def writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, true) }
+
+  def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) }
+  def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) }
+  def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) }
 
 
   /* diagnostics */