--- a/src/Tools/VSCode/src/channel.scala Wed Dec 21 11:55:59 2016 +0100
+++ b/src/Tools/VSCode/src/channel.scala Wed Dec 21 16:02:52 2016 +0100
@@ -86,4 +86,17 @@
out.flush
}
}
+
+
+ /* display message */
+
+ def display_message(message_type: Int, message: String, show: Boolean = true): Unit =
+ write(Protocol.DisplayMessage(message_type, message, 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)
}
--- a/src/Tools/VSCode/src/server.scala Wed Dec 21 11:55:59 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala Wed Dec 21 16:02:52 2016 +0100
@@ -106,11 +106,9 @@
def reply(err: String)
{
channel.write(Protocol.Initialize.reply(id, err))
- if (err == "") {
- channel.write(Protocol.DisplayMessage(Protocol.MessageType.Info,
- "Welcome to Isabelle/" + session_name + " (" + Distribution.version + ")"))
- }
- else channel.write(Protocol.DisplayMessage(Protocol.MessageType.Error, err))
+ if (err == "")
+ channel.writeln("Welcome to Isabelle/" + session_name + " (" + Distribution.version + ")")
+ else channel.error_message(err)
}
// FIXME handle error