proper order of matches: Server.Error is an instance of Exn.ERROR;
authorwenzelm
Wed Mar 21 18:30:17 2018 +0100 (14 months ago)
changeset 67913d58fa3ed236f
parent 67912 a7731d581bbc
child 67914 9f82f6cc3bfc
proper order of matches: Server.Error is an instance of Exn.ERROR;
src/Pure/Tools/server.scala
     1.1 --- a/src/Pure/Tools/server.scala	Wed Mar 21 17:55:17 2018 +0100
     1.2 +++ b/src/Pure/Tools/server.scala	Wed Mar 21 18:30:17 2018 +0100
     1.3 @@ -115,8 +115,8 @@
     1.4  
     1.5    def json_error(exn: Throwable): JSON.Object.T =
     1.6      exn match {
     1.7 +      case e: Error => Reply.error_message(e.message) ++ e.json
     1.8        case ERROR(msg) => Reply.error_message(msg)
     1.9 -      case e: Error => Reply.error_message(e.message) ++ e.json
    1.10        case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn))
    1.11        case _ => JSON.Object.empty
    1.12      }