# HG changeset patch
# User wenzelm
# Date 1482332572 -3600
# Node ID c231206a84c8a3b21f15ca65b36c5d584cfb4aca
# Parent  7b9196394b3237d497e948d676b35f69ca9ca24f
display messages, according to regular Isabelle Output;

diff -r 7b9196394b32 -r c231206a84c8 src/Tools/VSCode/src/channel.scala
--- 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)
 }
diff -r 7b9196394b32 -r c231206a84c8 src/Tools/VSCode/src/server.scala
--- 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