# HG changeset patch
# User wenzelm
# Date 1521042736 -3600
# Node ID 262d62a4c32bc238382a7634ed1241d275904fec
# Parent  ec9f1ec763a01e7f14f9e084e5f22b04053a8a71
more informative error with JSON result;
tuned signature;

diff -r ec9f1ec763a0 -r 262d62a4c32b src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Wed Mar 14 16:48:05 2018 +0100
+++ b/src/Pure/General/json.scala	Wed Mar 14 16:52:16 2018 +0100
@@ -19,10 +19,12 @@
 
   object Object
   {
+    type Entry = (String, JSON.T)
+
     type T = Map[String, JSON.T]
     val empty: Object.T = Map.empty
 
-    def apply(entries: (String, JSON.T)*): Object.T = Map(entries:_*)
+    def apply(entries: Entry*): Object.T = Map(entries:_*)
 
     def unapply(obj: T): Option[Object.T] =
       obj match {
diff -r ec9f1ec763a0 -r 262d62a4c32b src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Wed Mar 14 16:48:05 2018 +0100
+++ b/src/Pure/Tools/server.scala	Wed Mar 14 16:52:16 2018 +0100
@@ -78,10 +78,15 @@
 
   /* output reply */
 
+  class Error(val message: String, val json: JSON.Object.T = JSON.Object.empty)
+    extends RuntimeException(message)
+
   object Reply extends Enumeration
   {
     val OK, ERROR, NOTE = Value
 
+    def message(msg: String): JSON.Object.Entry = ("message" -> msg)
+
     def unapply(msg: String): Option[(Reply.Value, Any)] =
     {
       if (msg == "") None
@@ -155,8 +160,8 @@
 
     def reply_ok(arg: Any) { reply(Server.Reply.OK, arg) }
     def reply_error(arg: Any) { reply(Server.Reply.ERROR, arg) }
-    def reply_error_message(message: String, more: (String, JSON.T)*): Unit =
-      reply_error(JSON.Object("message" -> message) ++ more)
+    def reply_error_message(message: String, more: JSON.Object.Entry*): Unit =
+      reply_error(JSON.Object(Reply.message(message)) ++ more)
 
     def notify(arg: Any) { reply(Server.Reply.NOTE, arg) }
   }
@@ -171,11 +176,11 @@
     def shutdown() { server.close() }
 
     def notify(arg: Any) { connection.notify(arg) }
-    def message(kind: String, msg: String, more: (String, JSON.T)*): Unit =
-      notify(JSON.Object(Markup.KIND -> kind, "message" -> msg) ++ more)
-    def writeln(msg: String, more: (String, JSON.T)*): Unit = message(Markup.WRITELN, msg, more:_*)
-    def warning(msg: String, more: (String, JSON.T)*): Unit = message(Markup.WARNING, msg, more:_*)
-    def error_message(msg: String, more: (String, JSON.T)*): Unit =
+    def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
+      notify(JSON.Object(Markup.KIND -> kind, Reply.message(msg)) ++ 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 =
       message(Markup.ERROR_MESSAGE, msg, more:_*)
 
     val logger: Connection_Logger = new Connection_Logger(context)
@@ -411,7 +416,10 @@
                       if (cmd.isDefinedAt((context, arg))) {
                         Exn.capture { cmd((context, arg)) } match {
                           case Exn.Res(res) => connection.reply_ok(res)
-                          case Exn.Exn(ERROR(msg)) => connection.reply_error(msg)
+                          case Exn.Exn(exn: Server.Error) =>
+                            connection.reply_error_message(exn.message, exn.json.toList:_*)
+                          case Exn.Exn(ERROR(msg)) =>
+                            connection.reply_error_message(msg)
                           case Exn.Exn(exn) => throw exn
                         }
                       }