# HG changeset patch
# User wenzelm
# Date 1488468219 -3600
# Node ID 11e332c4e39f6a021e202e089a36cb7bd77f8eab
# Parent  548efa2bda664b4ba596f54870de8dadac2e2ba9
clarified errors;

diff -r 548efa2bda66 -r 11e332c4e39f 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)
       })