diff --git a/src/Pure/General/http.scala b/src/Pure/General/http.scala --- a/src/Pure/General/http.scala +++ b/src/Pure/General/http.scala @@ -1,292 +1,289 @@ /* Title: Pure/General/http.scala Author: Makarius HTTP server support. */ package isabelle import java.io.{File => JFile} import java.net.{InetSocketAddress, URI, URL, URLConnection, HttpURLConnection} import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer} object HTTP { /** content **/ val mime_type_bytes: String = "application/octet-stream" val mime_type_text: String = "text/plain; charset=utf-8" val mime_type_html: String = "text/html; charset=utf-8" val default_mime_type: String = mime_type_bytes val default_encoding: String = UTF8.charset_name sealed case class Content( bytes: Bytes, file_name: String = "", mime_type: String = default_mime_type, encoding: String = default_encoding) { def text: String = new String(bytes.array, encoding) } def read_content(file: JFile): Content = { val bytes = Bytes.read(file) val file_name = file.getName val mime_type = Option(URLConnection.guessContentTypeFromName(file_name)).getOrElse(default_mime_type) Content(bytes, file_name = file_name, mime_type = mime_type) } def read_content(path: Path): Content = read_content(path.file) /** client **/ val NEWLINE: String = "\r\n" object Client { - def set_user_agent(connection: URLConnection, user_agent: String): Unit = - proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s)) + def open_connection(url: URL, user_agent: String = ""): HttpURLConnection = + { + url.openConnection match { + case connection: HttpURLConnection => + proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s)) + connection + case _ => error("Bad URL (not HTTP): " + quote(url.toString)) + } + } - def get_content(connection: URLConnection): Content = + def get_content(connection: HttpURLConnection): Content = { val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r using(connection.getInputStream)(stream => { val bytes = Bytes.read_stream(stream, hint = connection.getContentLength) val file_name = Url.file_name(connection.getURL) val mime_type = Option(connection.getContentType).getOrElse(default_mime_type) val encoding = (connection.getContentEncoding, mime_type) match { case (enc, _) if enc != null => enc case (_, Charset(enc)) => enc case _ => default_encoding } Content(bytes, file_name = file_name, mime_type = mime_type, encoding = encoding) }) } def get(url: URL, user_agent: String = ""): Content = - { - val connection = url.openConnection - set_user_agent(connection, user_agent) - get_content(connection) - } + get_content(open_connection(url, user_agent = user_agent)) def post(url: URL, parameters: List[(String, Any)], user_agent: String = ""): Content = { - val connection = url.openConnection - connection match { - case http_connection: HttpURLConnection => - http_connection.setRequestMethod("POST") - connection.setDoOutput(true) - - set_user_agent(connection, user_agent) - - val boundary = UUID.random_string() - connection.setRequestProperty( - "Content-Type", "multipart/form-data; boundary=" + quote(boundary)) + val connection = open_connection(url, user_agent = user_agent) + connection.setRequestMethod("POST") + connection.setDoOutput(true) - using(connection.getOutputStream)(out => - { - def output(s: String): Unit = out.write(UTF8.bytes(s)) - def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE)) - def output_boundary(end: Boolean = false): Unit = - output("--" + boundary + (if (end) "--" else "") + NEWLINE) - def output_name(name: String): Unit = - output("Content-Disposition: form-data; name=" + quote(name)) - def output_value(value: Any): Unit = - { - output_newline(2) - output(value.toString) - } - def output_content(content: Content): Unit = - { - proper_string(content.file_name).foreach(s => output("; filename=" + quote(s))) - output_newline() - proper_string(content.mime_type).foreach(s => output("Content-Type: " + s)) - output_newline(2) - content.bytes.write_stream(out) - } + val boundary = UUID.random_string() + connection.setRequestProperty( + "Content-Type", "multipart/form-data; boundary=" + quote(boundary)) - output_newline(2) + using(connection.getOutputStream)(out => + { + def output(s: String): Unit = out.write(UTF8.bytes(s)) + def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE)) + def output_boundary(end: Boolean = false): Unit = + output("--" + boundary + (if (end) "--" else "") + NEWLINE) + def output_name(name: String): Unit = + output("Content-Disposition: form-data; name=" + quote(name)) + def output_value(value: Any): Unit = + { + output_newline(2) + output(value.toString) + } + def output_content(content: Content): Unit = + { + proper_string(content.file_name).foreach(s => output("; filename=" + quote(s))) + output_newline() + proper_string(content.mime_type).foreach(s => output("Content-Type: " + s)) + output_newline(2) + content.bytes.write_stream(out) + } - for { (name, value) <- parameters } { - output_boundary() - output_name(name) - value match { - case content: Content => output_content(content) - case file: JFile => output_content(read_content(file)) - case path: Path => output_content(read_content(path)) - case _ => output_value(value) - } - output_newline() - } - output_boundary(end = true) - out.flush() - }) - get_content(connection) + output_newline(2) - case _ => error("Bad URL (not HTTP): " + quote(url.toString)) - } + for { (name, value) <- parameters } { + output_boundary() + output_name(name) + value match { + case content: Content => output_content(content) + case file: JFile => output_content(read_content(file)) + case path: Path => output_content(read_content(path)) + case _ => output_value(value) + } + output_newline() + } + output_boundary(end = true) + out.flush() + }) + + get_content(connection) } } /** server **/ /* response */ object Response { def apply( bytes: Bytes = Bytes.empty, content_type: String = mime_type_bytes): Response = new Response(bytes, content_type) val empty: Response = apply() def text(s: String): Response = apply(Bytes(s), mime_type_text) def html(s: String): Response = apply(Bytes(s), mime_type_html) } class Response private[HTTP](val bytes: Bytes, val content_type: String) { override def toString: String = bytes.toString } /* exchange */ class Exchange private[HTTP](val http_exchange: HttpExchange) { def request_method: String = http_exchange.getRequestMethod def request_uri: URI = http_exchange.getRequestURI def read_request(): Bytes = using(http_exchange.getRequestBody)(Bytes.read_stream(_)) def write_response(code: Int, response: Response): Unit = { http_exchange.getResponseHeaders().set("Content-Type", response.content_type) http_exchange.sendResponseHeaders(code, response.bytes.length.toLong) using(http_exchange.getResponseBody)(response.bytes.write_stream(_)) } } /* handler for request method */ sealed case class Arg(method: String, uri: URI, request: Bytes) { def decode_properties: Properties.T = space_explode('&', request.text).map(s => space_explode('=', s) match { case List(a, b) => Url.decode(a) -> Url.decode(b) case _ => error("Malformed key-value pair in HTTP/POST: " + quote(s)) }) } object Handler { def apply(root: String, body: Exchange => Unit): Handler = new Handler(root, new HttpHandler { def handle(x: HttpExchange): Unit = body(new Exchange(x)) }) def method(name: String, root: String, body: Arg => Option[Response]): Handler = apply(root, http => { val request = http.read_request() if (http.request_method == name) { val arg = Arg(name, http.request_uri, request) Exn.capture(body(arg)) 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_message_text(msg))) case Exn.Exn(exn) => throw exn } } else http.write_response(400, Response.empty) }) def get(root: String, body: Arg => Option[Response]): Handler = method("GET", root, body) def post(root: String, body: Arg => Option[Response]): Handler = method("POST", root, body) } class Handler private(val root: String, val handler: HttpHandler) { override def toString: String = root } /* server */ class Server private[HTTP](val http_server: HttpServer) { def += (handler: Handler): Unit = http_server.createContext(handler.root, handler.handler) def -= (handler: Handler): Unit = http_server.removeContext(handler.root) def start(): Unit = http_server.start def stop(): Unit = http_server.stop(0) def address: InetSocketAddress = http_server.getAddress def url: String = "http://" + address.getHostName + ":" + address.getPort override def toString: String = url } def server(handlers: List[Handler] = isabelle_resources): Server = { val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0) http_server.setExecutor(null) val server = new Server(http_server) for (handler <- handlers) server += handler server } /** Isabelle resources **/ lazy val isabelle_resources: List[Handler] = List(welcome, fonts()) /* welcome */ val welcome: Handler = Handler.get("/", arg => if (arg.uri.toString == "/") { val id = Isabelle_System.isabelle_id() Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version)) } else None) /* fonts */ private lazy val html_fonts: List[Isabelle_Fonts.Entry] = Isabelle_Fonts.fonts(hidden = true) def fonts(root: String = "/fonts"): Handler = Handler.get(root, arg => { val uri_name = arg.uri.toString if (uri_name == root) { Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name)))) } else { html_fonts.collectFirst( { case entry if uri_name == root + "/" + entry.path.file_name => Response(entry.bytes) }) } }) }