1.1 --- a/src/Tools/VSCode/src/channel.scala	Wed Dec 21 11:55:59 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/channel.scala	Wed Dec 21 16:02:52 2016 +0100
     1.3 @@ -86,4 +86,17 @@
     1.4        out.flush
     1.5      }
     1.6    }
     1.7 +
     1.8 +
     1.9 +  /* display message */
    1.10 +
    1.11 +  def display_message(message_type: Int, message: String, show: Boolean = true): Unit =
    1.12 +    write(Protocol.DisplayMessage(message_type, message, show))
    1.13 +
    1.14 +  def error_message(message: String, show: Boolean = true): Unit =
    1.15 +    display_message(Protocol.MessageType.Error, message, show)
    1.16 +  def warning(message: String, show: Boolean = true): Unit =
    1.17 +    display_message(Protocol.MessageType.Warning, message, show)
    1.18 +  def writeln(message: String, show: Boolean = true): Unit =
    1.19 +    display_message(Protocol.MessageType.Info, message, show)
    1.20  }

     2.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 21 11:55:59 2016 +0100
     2.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 21 16:02:52 2016 +0100
     2.3 @@ -106,11 +106,9 @@
     2.4      def reply(err: String)
     2.5      {
     2.6        channel.write(Protocol.Initialize.reply(id, err))
     2.7 -      if (err == "") {
     2.8 -        channel.write(Protocol.DisplayMessage(Protocol.MessageType.Info,
     2.9 -          "Welcome to Isabelle/" + session_name + " (" + Distribution.version + ")"))
    2.10 -      }
    2.11 -      else channel.write(Protocol.DisplayMessage(Protocol.MessageType.Error, err))
    2.12 +      if (err == "")
    2.13 +        channel.writeln("Welcome to Isabelle/" + session_name + " (" + Distribution.version + ")")
    2.14 +      else channel.error_message(err)
    2.15      }
    2.16  
    2.17      // FIXME handle error