clarified markup according to common Command.Results;
authorwenzelm
Wed Mar 21 13:17:30 2018 +0100 (14 months ago)
changeset 679113cda747493d8
parent 67906 9cc32b18c785
child 67912 a7731d581bbc
clarified markup according to common Command.Results;
src/Pure/Tools/server.scala
     1.1 --- a/src/Pure/Tools/server.scala	Tue Mar 20 09:27:40 2018 +0000
     1.2 +++ b/src/Pure/Tools/server.scala	Wed Mar 21 13:17:30 2018 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4        else JSON.Object(Markup.KIND -> kind, "message" -> msg)
     1.5  
     1.6      def error_message(msg: String): JSON.Object.T =
     1.7 -      message(msg, kind = Markup.ERROR_MESSAGE)
     1.8 +      message(msg, kind = Markup.ERROR)
     1.9  
    1.10      def unapply(msg: String): Option[(Reply.Value, Any)] =
    1.11      {
    1.12 @@ -225,7 +225,7 @@
    1.13      def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*)
    1.14      def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*)
    1.15      def error_message(msg: String, more: JSON.Object.Entry*): Unit =
    1.16 -      message(Markup.ERROR_MESSAGE, msg, more:_*)
    1.17 +      message(Markup.ERROR, msg, more:_*)
    1.18  
    1.19      def progress(more: JSON.Object.Entry*): Connection_Progress =
    1.20        new Connection_Progress(context, more:_*)