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,195 +1,292 @@ /* Title: Pure/General/http.scala Author: Makarius HTTP server support. */ package isabelle -import java.net.{InetSocketAddress, URI, URL} +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 default_mime_type: String = "application/octet-stream" + 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" - sealed case class Content(bytes: Bytes, mime_type: String = default_mime_type) + 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 = bytes.text + 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 get(url: URL): Content = + def set_user_agent(connection: URLConnection, user_agent: String): Unit = + proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s)) + + def get_content(connection: URLConnection): 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 - using(connection.getInputStream)(stream => - { - val length = connection.getContentLength - val mime_type = Option(connection.getContentType).getOrElse(default_mime_type) - val bytes = Bytes.read_stream(stream, hint = length) - Content(bytes, mime_type = mime_type) - }) + set_user_agent(connection, user_agent) + get_content(connection) + } + + 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)) + + 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) + } + + output_newline(2) + + 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) + + case _ => error("Bad URL (not HTTP): " + quote(url.toString)) + } } } /** server **/ /* response */ object Response { def apply( bytes: Bytes = Bytes.empty, - content_type: String = "application/octet-stream"): Response = + content_type: String = mime_type_bytes): Response = new Response(bytes, content_type) val empty: Response = apply() - def text(s: String): Response = apply(Bytes(s), "text/plain; charset=utf-8") - def html(s: String): Response = apply(Bytes(s), "text/html; charset=utf-8") + 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) }) } }) } diff --git a/src/Pure/General/url.scala b/src/Pure/General/url.scala --- a/src/Pure/General/url.scala +++ b/src/Pure/General/url.scala @@ -1,103 +1,106 @@ /* Title: Pure/General/url.scala Author: Makarius Basic URL operations. */ package isabelle import java.io.{File => JFile} import java.nio.file.{Paths, FileSystemNotFoundException} import java.net.{URI, URISyntaxException, URL, MalformedURLException, URLDecoder, URLEncoder} import java.util.Locale import java.util.zip.GZIPInputStream object Url { /* special characters */ def escape_special(c: Char): String = if ("!#$&'()*+,/:;=?@[]".contains(c)) { String.format(Locale.ROOT, "%%%02X", Integer.valueOf(c.toInt)) } else c.toString def escape_special(s: String): String = s.iterator.map(escape_special).mkString def escape_name(name: String): String = name.iterator.map({ case '\'' => "%27" case c => c.toString }).mkString /* make and check URLs */ def apply(name: String): URL = { try { new URL(name) } catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) } } def is_wellformed(name: String): Boolean = try { Url(name); true } catch { case ERROR(_) => false } def is_readable(name: String): Boolean = try { Url(name).openStream.close(); true } catch { case ERROR(_) => false } - /* trim index */ + /* file name */ + + def file_name(url: URL): String = + Library.take_suffix[Char](c => c != '/' && c != '\\', url.getFile.toString.toList)._2.mkString def trim_index(url: URL): URL = { Library.try_unprefix("/index.html", url.toString) match { case Some(u) => Url(u) case None => Library.try_unprefix("/index.php", url.toString) match { case Some(u) => Url(u) case None => url } } } /* strings */ def decode(s: String): String = URLDecoder.decode(s, UTF8.charset_name) def encode(s: String): String = URLEncoder.encode(s, UTF8.charset_name) /* read */ private def read(url: URL, gzip: Boolean): String = using(url.openStream)(stream => File.read_stream(if (gzip) new GZIPInputStream(stream) else stream)) def read(url: URL): String = read(url, false) def read_gzip(url: URL): String = read(url, true) def read(name: String): String = read(Url(name), false) def read_gzip(name: String): String = read(Url(name), true) /* file URIs */ def print_file(file: JFile): String = File.absolute(file).toPath.toUri.toString def print_file_name(name: String): String = print_file(new JFile(name)) def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile def is_wellformed_file(uri: String): Boolean = try { parse_file(uri); true } catch { case _: URISyntaxException | _: IllegalArgumentException | _: FileSystemNotFoundException => false } def absolute_file(uri: String): JFile = File.absolute(parse_file(uri)) def absolute_file_name(uri: String): String = absolute_file(uri).getPath def canonical_file(uri: String): JFile = File.canonical(parse_file(uri)) def canonical_file_name(uri: String): String = canonical_file(uri).getPath }