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