# HG changeset patch
# User wenzelm
# Date 1521303207 -3600
# Node ID 4f383cd54f699771a69b16c569de0b2b996074c4
# Parent  f4a505d6bc94765aa83e648c4076d4e5e6ad4616
clarified exception handling: include interrupts;

diff -r f4a505d6bc94 -r 4f383cd54f69 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Mar 17 16:32:50 2018 +0100
+++ b/src/Pure/Tools/server.scala	Sat Mar 17 17:13:27 2018 +0100
@@ -111,6 +111,14 @@
   class Error(val message: String, val json: JSON.Object.T = JSON.Object.empty)
     extends RuntimeException(message)
 
+  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 _ => JSON.Object.empty
+    }
+
   object Reply extends Enumeration
   {
     val OK, ERROR, FINISHED, FAILED, NOTE = Value
@@ -274,11 +282,9 @@
       Exn.capture { body(task) } match {
         case Exn.Res(res) =>
           context.reply(Reply.FINISHED, res + ident)
-        case Exn.Exn(exn: Server.Error) =>
-          context.reply(Reply.FAILED, JSON.Object(Reply.message(exn.message)) ++ exn.json + ident)
-        case Exn.Exn(ERROR(msg)) =>
-          context.reply(Reply.FAILED, JSON.Object(Reply.message(msg)) + ident)
-        case Exn.Exn(exn) => throw exn
+        case Exn.Exn(exn) =>
+          val err = json_error(exn)
+          if (err.isEmpty) throw exn else context.reply(Reply.FAILED, err + ident)
       }
       progress.stop
       context.remove_task(task)
@@ -524,11 +530,9 @@
                               connection.reply_ok(JSON.Object(task.ident))
                               task.start
                             case Exn.Res(res) => connection.reply_ok(res)
-                            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
+                            case Exn.Exn(exn) =>
+                              val err = Server.json_error(exn)
+                              if (err.isEmpty) throw exn else connection.reply_error(err)
                           }
                         }
                         else {