clarified exception handling: include interrupts;
authorwenzelm
Sat Mar 17 17:13:27 2018 +0100 (14 months ago)
changeset 678914f383cd54f69
parent 67890 f4a505d6bc94
child 67892 25e2b621bdcb
clarified exception handling: include interrupts;
src/Pure/Tools/server.scala
     1.1 --- a/src/Pure/Tools/server.scala	Sat Mar 17 16:32:50 2018 +0100
     1.2 +++ b/src/Pure/Tools/server.scala	Sat Mar 17 17:13:27 2018 +0100
     1.3 @@ -111,6 +111,14 @@
     1.4    class Error(val message: String, val json: JSON.Object.T = JSON.Object.empty)
     1.5      extends RuntimeException(message)
     1.6  
     1.7 +  def json_error(exn: Throwable): JSON.Object.T =
     1.8 +    exn match {
     1.9 +      case ERROR(msg) => JSON.Object(Reply.message(msg))
    1.10 +      case e: Error => JSON.Object(Reply.message(e.message)) ++ e.json
    1.11 +      case _ if Exn.is_interrupt(exn) => JSON.Object(Reply.message(Exn.message(exn)))
    1.12 +      case _ => JSON.Object.empty
    1.13 +    }
    1.14 +
    1.15    object Reply extends Enumeration
    1.16    {
    1.17      val OK, ERROR, FINISHED, FAILED, NOTE = Value
    1.18 @@ -274,11 +282,9 @@
    1.19        Exn.capture { body(task) } match {
    1.20          case Exn.Res(res) =>
    1.21            context.reply(Reply.FINISHED, res + ident)
    1.22 -        case Exn.Exn(exn: Server.Error) =>
    1.23 -          context.reply(Reply.FAILED, JSON.Object(Reply.message(exn.message)) ++ exn.json + ident)
    1.24 -        case Exn.Exn(ERROR(msg)) =>
    1.25 -          context.reply(Reply.FAILED, JSON.Object(Reply.message(msg)) + ident)
    1.26 -        case Exn.Exn(exn) => throw exn
    1.27 +        case Exn.Exn(exn) =>
    1.28 +          val err = json_error(exn)
    1.29 +          if (err.isEmpty) throw exn else context.reply(Reply.FAILED, err + ident)
    1.30        }
    1.31        progress.stop
    1.32        context.remove_task(task)
    1.33 @@ -524,11 +530,9 @@
    1.34                                connection.reply_ok(JSON.Object(task.ident))
    1.35                                task.start
    1.36                              case Exn.Res(res) => connection.reply_ok(res)
    1.37 -                            case Exn.Exn(exn: Server.Error) =>
    1.38 -                              connection.reply_error_message(exn.message, exn.json.toList:_*)
    1.39 -                            case Exn.Exn(ERROR(msg)) =>
    1.40 -                              connection.reply_error_message(msg)
    1.41 -                            case Exn.Exn(exn) => throw exn
    1.42 +                            case Exn.Exn(exn) =>
    1.43 +                              val err = Server.json_error(exn)
    1.44 +                              if (err.isEmpty) throw exn else connection.reply_error(err)
    1.45                            }
    1.46                          }
    1.47                          else {