# HG changeset patch
# User wenzelm
# Date 1521634650 -3600
# Node ID 3cda747493d8049d8d26b02217574dd4f1b47ae9
# Parent  9cc32b18c7851f560a87546c0eda6052785bf38d
clarified markup according to common Command.Results;

diff -r 9cc32b18c785 -r 3cda747493d8 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Tue Mar 20 09:27:40 2018 +0000
+++ b/src/Pure/Tools/server.scala	Wed Mar 21 13:17:30 2018 +0100
@@ -130,7 +130,7 @@
       else JSON.Object(Markup.KIND -> kind, "message" -> msg)
 
     def error_message(msg: String): JSON.Object.T =
-      message(msg, kind = Markup.ERROR_MESSAGE)
+      message(msg, kind = Markup.ERROR)
 
     def unapply(msg: String): Option[(Reply.Value, Any)] =
     {
@@ -225,7 +225,7 @@
     def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*)
     def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*)
     def error_message(msg: String, more: JSON.Object.Entry*): Unit =
-      message(Markup.ERROR_MESSAGE, msg, more:_*)
+      message(Markup.ERROR, msg, more:_*)
 
     def progress(more: JSON.Object.Entry*): Connection_Progress =
       new Connection_Progress(context, more:_*)