author | wenzelm |
Wed, 21 Mar 2018 18:30:17 +0100 | |
changeset 67913 | d58fa3ed236f |
parent 67912 | a7731d581bbc |
child 67914 | 9f82f6cc3bfc |
--- a/src/Pure/Tools/server.scala Wed Mar 21 17:55:17 2018 +0100 +++ b/src/Pure/Tools/server.scala Wed Mar 21 18:30:17 2018 +0100 @@ -115,8 +115,8 @@ def json_error(exn: Throwable): JSON.Object.T = exn match { + case e: Error => Reply.error_message(e.message) ++ e.json 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 }