1/* Title: Pure/General/http.scala 2 Author: Makarius 3 4HTTP server support. 5*/ 6 7package isabelle 8 9 10import java.net.{InetAddress, InetSocketAddress, URI} 11import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer} 12 13import scala.collection.immutable.SortedMap 14 15 16object HTTP 17{ 18 /** server **/ 19 20 /* response */ 21 22 object Response 23 { 24 def apply( 25 bytes: Bytes = Bytes.empty, 26 content_type: String = "application/octet-stream"): Response = 27 new Response(bytes, content_type) 28 29 val empty: Response = apply() 30 def text(s: String): Response = apply(Bytes(s), "text/plain; charset=utf-8") 31 def html(s: String): Response = apply(Bytes(s), "text/html; charset=utf-8") 32 } 33 34 class Response private[HTTP](val bytes: Bytes, val content_type: String) 35 { 36 override def toString: String = bytes.toString 37 } 38 39 40 /* exchange */ 41 42 class Exchange private[HTTP](val http_exchange: HttpExchange) 43 { 44 def request_method: String = http_exchange.getRequestMethod 45 def request_uri: URI = http_exchange.getRequestURI 46 47 def read_request(): Bytes = 48 using(http_exchange.getRequestBody)(Bytes.read_stream(_)) 49 50 def write_response(code: Int, response: Response) 51 { 52 http_exchange.getResponseHeaders().set("Content-Type", response.content_type) 53 http_exchange.sendResponseHeaders(code, response.bytes.length.toLong) 54 using(http_exchange.getResponseBody)(response.bytes.write_stream(_)) 55 } 56 } 57 58 59 /* handler */ 60 61 class Handler private[HTTP](val root: String, val handler: HttpHandler) 62 { 63 override def toString: String = root 64 } 65 66 def handler(root: String, body: Exchange => Unit): Handler = 67 new Handler(root, new HttpHandler { def handle(x: HttpExchange) { body(new Exchange(x)) } }) 68 69 70 /* particular methods */ 71 72 sealed case class Arg(method: String, uri: URI, request: Bytes) 73 { 74 def decode_properties: Properties.T = 75 space_explode('&', request.text).map(s => 76 space_explode('=', s) match { 77 case List(a, b) => Url.decode(a) -> Url.decode(b) 78 case _ => error("Malformed key-value pair in HTTP/POST: " + quote(s)) 79 }) 80 } 81 82 def method(name: String, root: String, body: Arg => Option[Response]): Handler = 83 handler(root, http => 84 { 85 val request = http.read_request() 86 if (http.request_method == name) { 87 val arg = Arg(name, http.request_uri, request) 88 Exn.capture(body(arg)) match { 89 case Exn.Res(Some(response)) => 90 http.write_response(200, response) 91 case Exn.Res(None) => 92 http.write_response(404, Response.empty) 93 case Exn.Exn(ERROR(msg)) => 94 http.write_response(500, Response.text(Output.error_message_text(msg))) 95 case Exn.Exn(exn) => throw exn 96 } 97 } 98 else http.write_response(400, Response.empty) 99 }) 100 101 def get(root: String, body: Arg => Option[Response]): Handler = method("GET", root, body) 102 def post(root: String, body: Arg => Option[Response]): Handler = method("POST", root, body) 103 104 105 /* server */ 106 107 class Server private[HTTP](val http_server: HttpServer) 108 { 109 def += (handler: Handler) { http_server.createContext(handler.root, handler.handler) } 110 def -= (handler: Handler) { http_server.removeContext(handler.root) } 111 112 def start: Unit = http_server.start 113 def stop: Unit = http_server.stop(0) 114 115 def address: InetSocketAddress = http_server.getAddress 116 def url: String = "http://" + address.getHostName + ":" + address.getPort 117 override def toString: String = url 118 } 119 120 def server(handlers: List[Handler] = isabelle_resources): Server = 121 { 122 val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0) 123 http_server.setExecutor(null) 124 125 val server = new Server(http_server) 126 for (handler <- handlers) server += handler 127 server 128 } 129 130 131 132 /** Isabelle resources **/ 133 134 lazy val isabelle_resources: List[Handler] = 135 List(welcome, fonts()) 136 137 138 /* welcome */ 139 140 val welcome: Handler = 141 get("/", arg => 142 if (arg.uri.toString == "/") { 143 val id = Isabelle_System.isabelle_id() 144 Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version)) 145 } 146 else None) 147 148 149 /* fonts */ 150 151 private lazy val html_fonts: List[Isabelle_Fonts.Entry] = 152 Isabelle_Fonts.fonts(hidden = true) 153 154 def fonts(root: String = "/fonts"): Handler = 155 get(root, arg => 156 { 157 val uri_name = arg.uri.toString 158 if (uri_name == root) { 159 Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name)))) 160 } 161 else { 162 html_fonts.collectFirst( 163 { case entry if uri_name == root + "/" + entry.path.file_name => Response(entry.bytes) }) 164 } 165 }) 166} 167