clarified errors;
authorwenzelm
Thu, 02 Mar 2017 16:23:39 +0100
changeset 65087 11e332c4e39f
parent 65086 548efa2bda66
child 65088 18f2d388fab4
clarified errors;
src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Mar 02 16:09:46 2017 +0100
+++ b/src/Pure/General/http.scala	Thu Mar 02 16:23:39 2017 +0100
@@ -71,9 +71,14 @@
       {
         http.read_request()
         if (http.request_method == "GET")
-          body(http.request_uri) match {
-            case None => http.write_response(404, Response.empty)
-            case Some(response) => http.write_response(200, response)
+          Exn.capture(body(http.request_uri)) match {
+            case Exn.Res(Some(response)) =>
+              http.write_response(200, response)
+            case Exn.Res(None) =>
+              http.write_response(404, Response.empty)
+            case Exn.Exn(ERROR(msg)) =>
+              http.write_response(500, Response.text(Output.error_text(msg)))
+            case Exn.Exn(exn) => throw exn
           }
         else http.write_response(400, Response.empty)
       })