src/Tools/VSCode/src/channel.scala
changeset 64686 7888be4fa496
parent 64675 c557279d93f2
child 64717 d2b50eb3d9ab
--- 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 */