equal
deleted
inserted
replaced
69 def get(root: String, body: URI => Option[Response]): Handler = |
69 def get(root: String, body: URI => Option[Response]): Handler = |
70 handler(root, http => |
70 handler(root, http => |
71 { |
71 { |
72 http.read_request() |
72 http.read_request() |
73 if (http.request_method == "GET") |
73 if (http.request_method == "GET") |
74 body(http.request_uri) match { |
74 Exn.capture(body(http.request_uri)) match { |
75 case None => http.write_response(404, Response.empty) |
75 case Exn.Res(Some(response)) => |
76 case Some(response) => http.write_response(200, response) |
76 http.write_response(200, response) |
|
77 case Exn.Res(None) => |
|
78 http.write_response(404, Response.empty) |
|
79 case Exn.Exn(ERROR(msg)) => |
|
80 http.write_response(500, Response.text(Output.error_text(msg))) |
|
81 case Exn.Exn(exn) => throw exn |
77 } |
82 } |
78 else http.write_response(400, Response.empty) |
83 else http.write_response(400, Response.empty) |
79 }) |
84 }) |
80 |
85 |
81 |
86 |