src/Pure/Tools/server.scala
changeset 67913 d58fa3ed236f
parent 67911 3cda747493d8
child 67920 c3c74310154e
equal deleted inserted replaced
67912:a7731d581bbc 67913:d58fa3ed236f
   113   class Error(val message: String, val json: JSON.Object.T = JSON.Object.empty)
   113   class Error(val message: String, val json: JSON.Object.T = JSON.Object.empty)
   114     extends RuntimeException(message)
   114     extends RuntimeException(message)
   115 
   115 
   116   def json_error(exn: Throwable): JSON.Object.T =
   116   def json_error(exn: Throwable): JSON.Object.T =
   117     exn match {
   117     exn match {
       
   118       case e: Error => Reply.error_message(e.message) ++ e.json
   118       case ERROR(msg) => Reply.error_message(msg)
   119       case ERROR(msg) => Reply.error_message(msg)
   119       case e: Error => Reply.error_message(e.message) ++ e.json
       
   120       case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn))
   120       case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn))
   121       case _ => JSON.Object.empty
   121       case _ => JSON.Object.empty
   122     }
   122     }
   123 
   123 
   124   object Reply extends Enumeration
   124   object Reply extends Enumeration