--- 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 */