more explicit error messages;
clarified signature;

--- a/src/Pure/Tools/server.scala	Sun Mar 18 11:42:57 2018 +0100
+++ b/src/Pure/Tools/server.scala	Sun Mar 18 12:11:30 2018 +0100
@@ -113,9 +113,9 @@
 
   def json_error(exn: Throwable): JSON.Object.T =
     exn match {
-      case ERROR(msg) => JSON.Object(Reply.message(msg))
-      case e: Error => JSON.Object(Reply.message(e.message)) ++ e.json
-      case _ if Exn.is_interrupt(exn) => JSON.Object(Reply.message(Exn.message(exn)))
+      case ERROR(msg) => Reply.error_message(msg)
+      case e: Error => Reply.error_message(e.message) ++ e.json
+      case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn))
       case _ => JSON.Object.empty
     }
 
@@ -123,7 +123,12 @@
   {
     val OK, ERROR, FINISHED, FAILED, NOTE = Value
 
-    def message(msg: String): JSON.Object.Entry = ("message" -> msg)
+    def message(msg: String, kind: String = ""): JSON.Object.T =
+      if (kind == "") JSON.Object("message" -> msg)
+      else JSON.Object(Markup.KIND -> kind, "message" -> msg)
+
+    def error_message(msg: String): JSON.Object.T =
+      message(msg, kind = Markup.ERROR_MESSAGE)
 
     def unapply(msg: String): Option[(Reply.Value, Any)] =
     {
@@ -199,7 +204,7 @@
     def reply_ok(arg: Any) { reply(Reply.OK, arg) }
     def reply_error(arg: Any) { reply(Reply.ERROR, arg) }
     def reply_error_message(message: String, more: JSON.Object.Entry*): Unit =
-      reply_error(JSON.Object(Reply.message(message)) ++ more)
+      reply_error(Reply.error_message(message) ++ more)
 
     def notify(arg: Any) { reply(Reply.NOTE, arg) }
   }
@@ -214,7 +219,7 @@
     def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) }
     def notify(arg: Any) { connection.notify(arg) }
     def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
-      notify(JSON.Object(Markup.KIND -> kind, Reply.message(msg)) ++ more)
+      notify(Reply.message(msg, kind = kind) ++ more)
     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 =

--- a/src/Pure/Tools/server_commands.scala	Sun Mar 18 11:42:57 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Sun Mar 18 12:11:30 2018 +0100
@@ -186,20 +186,18 @@
         session.use_theories(args.theories, qualifier = args.qualifier,
           master_dir = args.master_dir, id = id, progress = progress)
 
-      def output_text(s: String): JSON.Object.Entry =
-        Server.Reply.message(if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s))
+      def output_text(s: String): String =
+        if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
 
       def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T =
       {
         val position = "pos" -> Position.JSON(pos)
         tree match {
-          case XML.Text(msg) => JSON.Object(output_text(msg), position)
+          case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position
           case elem: XML.Elem =>
             val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
-            Markup.messages.collectFirst({ case (a, b) if b == elem.name => a }) match {
-              case None => JSON.Object(output_text(msg), position)
-              case Some(kind) => JSON.Object(Markup.KIND -> kind, output_text(msg), position)
-            }
+            val kind = Markup.messages.collectFirst({ case (a, b) if b == elem.name => a })
+            Server.Reply.message(output_text(msg), kind = kind getOrElse "") + position
         }
       }