src/Pure/General/http.scala
changeset 80201 6ac48d53d371
parent 79717 da4e82434985
child 80202 03c058592c58
equal deleted inserted replaced
80200:5f053991315c 80201:6ac48d53d371
   218   }
   218   }
   219 
   219 
   220   class Response private[HTTP](val output: Bytes, val content_type: String) {
   220   class Response private[HTTP](val output: Bytes, val content_type: String) {
   221     override def toString: String = output.toString
   221     override def toString: String = output.toString
   222 
   222 
   223     def write(http: HttpExchange, code: Int): Unit = {
   223     def write(http: HttpExchange, code: Int, is_head: Boolean = false): Unit = {
   224       http.getResponseHeaders.set("Content-Type", content_type)
   224       http.getResponseHeaders.set("Content-Type", content_type)
   225       http.sendResponseHeaders(code, output.length.toLong)
   225       http.sendResponseHeaders(code, if (is_head) -1 else output.length.toLong)
   226       using(http.getResponseBody)(output.write_stream)
   226       if (!is_head) using(http.getResponseBody)(output.write_stream)
   227     }
   227     }
   228   }
   228   }
   229 
   229 
   230 
   230 
   231   /* service */
   231   /* service */
   239       proper_string(url_path(server_name, name)).getOrElse("/")
   239       proper_string(url_path(server_name, name)).getOrElse("/")
   240 
   240 
   241     def handler(server_name: String): HttpHandler = { (http: HttpExchange) =>
   241     def handler(server_name: String): HttpHandler = { (http: HttpExchange) =>
   242       val uri = http.getRequestURI
   242       val uri = http.getRequestURI
   243       val input = using(http.getRequestBody)(Bytes.read_stream(_))
   243       val input = using(http.getRequestBody)(Bytes.read_stream(_))
   244       if (http.getRequestMethod == method) {
   244       val is_head = http.getRequestMethod == "HEAD" && method == "GET"
       
   245       if (http.getRequestMethod == method || is_head) {
   245         val request = new Request(server_name, name, uri, input)
   246         val request = new Request(server_name, name, uri, input)
   246         Exn.result(apply(request)) match {
   247         Exn.result(apply(request)) match {
   247           case Exn.Res(Some(response)) =>
   248           case Exn.Res(Some(response)) =>
   248             response.write(http, 200)
   249             response.write(http, 200, is_head)
   249           case Exn.Res(None) =>
   250           case Exn.Res(None) =>
   250             Response.empty.write(http, 404)
   251             Response.empty.write(http, 404, is_head)
   251           case Exn.Exn(ERROR(msg)) =>
   252           case Exn.Exn(ERROR(msg)) =>
   252             Response.text(Output.error_message_text(msg)).write(http, 500)
   253             Response.text(Output.error_message_text(msg)).write(http, 500, is_head)
   253           case Exn.Exn(exn) => throw exn
   254           case Exn.Exn(exn) => throw exn
   254         }
   255         }
   255       }
   256       }
   256       else Response.empty.write(http, 400)
   257       else Response.empty.write(http, 400)
   257     }
   258     }