# HG changeset patch
# User wenzelm
# Date 1521653417 -3600
# Node ID d58fa3ed236ff9bbfbee747adb00b9d9d179b41e
# Parent  a7731d581bbc4ff0f625c550eb79e4c7e7887051
proper order of matches: Server.Error is an instance of Exn.ERROR;

diff -r a7731d581bbc -r d58fa3ed236f src/Pure/Tools/server.scala
--- 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
     }