author | wenzelm |
Wed, 28 Nov 2018 14:51:24 +0100 | |
changeset 69363 | 0675481ce575 |
parent 69360 | dc9a39c3f75d |
child 69364 | 91dbade9a5fa |
permissions | -rw-r--r-- |
65077 | 1 |
/* Title: Pure/General/http.scala |
63823 | 2 |
Author: Makarius |
3 |
||
65077 | 4 |
HTTP server support. |
63823 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
67245 | 10 |
import java.net.{InetAddress, InetSocketAddress, URI} |
63823 | 11 |
import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer} |
12 |
||
65079 | 13 |
import scala.collection.immutable.SortedMap |
14 |
||
63823 | 15 |
|
65077 | 16 |
object HTTP |
63823 | 17 |
{ |
65081 | 18 |
/** server **/ |
19 |
||
65078 | 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 = |
|
69305
5a71b5145201
prefer statically-typed close operation, avoid Java 11 warning: "Illegal reflective access by scala.reflect.package$ to method sun.net.httpserver.LeftOverInputStream.close()";
wenzelm
parents:
67865
diff
changeset
|
48 |
{ |
5a71b5145201
prefer statically-typed close operation, avoid Java 11 warning: "Illegal reflective access by scala.reflect.package$ to method sun.net.httpserver.LeftOverInputStream.close()";
wenzelm
parents:
67865
diff
changeset
|
49 |
val stream = http_exchange.getRequestBody |
5a71b5145201
prefer statically-typed close operation, avoid Java 11 warning: "Illegal reflective access by scala.reflect.package$ to method sun.net.httpserver.LeftOverInputStream.close()";
wenzelm
parents:
67865
diff
changeset
|
50 |
try { Bytes.read_stream(stream) } finally { stream.close } |
5a71b5145201
prefer statically-typed close operation, avoid Java 11 warning: "Illegal reflective access by scala.reflect.package$ to method sun.net.httpserver.LeftOverInputStream.close()";
wenzelm
parents:
67865
diff
changeset
|
51 |
} |
65078 | 52 |
|
53 |
def write_response(code: Int, response: Response) |
|
54 |
{ |
|
55 |
http_exchange.getResponseHeaders().set("Content-Type", response.content_type) |
|
56 |
http_exchange.sendResponseHeaders(code, response.bytes.length.toLong) |
|
69305
5a71b5145201
prefer statically-typed close operation, avoid Java 11 warning: "Illegal reflective access by scala.reflect.package$ to method sun.net.httpserver.LeftOverInputStream.close()";
wenzelm
parents:
67865
diff
changeset
|
57 |
|
5a71b5145201
prefer statically-typed close operation, avoid Java 11 warning: "Illegal reflective access by scala.reflect.package$ to method sun.net.httpserver.LeftOverInputStream.close()";
wenzelm
parents:
67865
diff
changeset
|
58 |
val stream = http_exchange.getResponseBody |
5a71b5145201
prefer statically-typed close operation, avoid Java 11 warning: "Illegal reflective access by scala.reflect.package$ to method sun.net.httpserver.LeftOverInputStream.close()";
wenzelm
parents:
67865
diff
changeset
|
59 |
try { response.bytes.write_stream(stream) } finally { stream.close } |
65078 | 60 |
} |
61 |
} |
|
62 |
||
63 |
||
65077 | 64 |
/* handler */ |
65 |
||
65080 | 66 |
class Handler private[HTTP](val root: String, val handler: HttpHandler) |
65076 | 67 |
{ |
65080 | 68 |
override def toString: String = root |
65076 | 69 |
} |
70 |
||
65080 | 71 |
def handler(root: String, body: Exchange => Unit): Handler = |
72 |
new Handler(root, new HttpHandler { def handle(x: HttpExchange) { body(new Exchange(x)) } }) |
|
65078 | 73 |
|
66207 | 74 |
|
75 |
/* particular methods */ |
|
76 |
||
77 |
sealed case class Arg(method: String, uri: URI, request: Bytes) |
|
78 |
{ |
|
79 |
def decode_properties: Properties.T = |
|
66923 | 80 |
space_explode('&', request.text).map(s => |
81 |
space_explode('=', s) match { |
|
67245 | 82 |
case List(a, b) => Url.decode(a) -> Url.decode(b) |
66207 | 83 |
case _ => error("Malformed key-value pair in HTTP/POST: " + quote(s)) |
84 |
}) |
|
85 |
} |
|
86 |
||
87 |
def method(name: String, root: String, body: Arg => Option[Response]): Handler = |
|
65080 | 88 |
handler(root, http => |
65078 | 89 |
{ |
66207 | 90 |
val request = http.read_request() |
91 |
if (http.request_method == name) { |
|
92 |
val arg = Arg(name, http.request_uri, request) |
|
93 |
Exn.capture(body(arg)) match { |
|
65087 | 94 |
case Exn.Res(Some(response)) => |
95 |
http.write_response(200, response) |
|
96 |
case Exn.Res(None) => |
|
97 |
http.write_response(404, Response.empty) |
|
98 |
case Exn.Exn(ERROR(msg)) => |
|
65828 | 99 |
http.write_response(500, Response.text(Output.error_message_text(msg))) |
65087 | 100 |
case Exn.Exn(exn) => throw exn |
65078 | 101 |
} |
66207 | 102 |
} |
65078 | 103 |
else http.write_response(400, Response.empty) |
104 |
}) |
|
65076 | 105 |
|
66207 | 106 |
def get(root: String, body: Arg => Option[Response]): Handler = method("GET", root, body) |
107 |
def post(root: String, body: Arg => Option[Response]): Handler = method("POST", root, body) |
|
108 |
||
65077 | 109 |
|
110 |
/* server */ |
|
111 |
||
112 |
class Server private[HTTP](val http_server: HttpServer) |
|
113 |
{ |
|
65080 | 114 |
def += (handler: Handler) { http_server.createContext(handler.root, handler.handler) } |
115 |
def -= (handler: Handler) { http_server.removeContext(handler.root) } |
|
65077 | 116 |
|
117 |
def start: Unit = http_server.start |
|
118 |
def stop: Unit = http_server.stop(0) |
|
119 |
||
120 |
def address: InetSocketAddress = http_server.getAddress |
|
121 |
def url: String = "http://" + address.getHostName + ":" + address.getPort |
|
122 |
override def toString: String = url |
|
123 |
} |
|
124 |
||
65081 | 125 |
def server(handlers: List[Handler] = isabelle_resources): Server = |
63823 | 126 |
{ |
127 |
val localhost = InetAddress.getByName("127.0.0.1") |
|
65077 | 128 |
val http_server = HttpServer.create(new InetSocketAddress(localhost, 0), 0) |
129 |
http_server.setExecutor(null) |
|
65076 | 130 |
|
65077 | 131 |
val server = new Server(http_server) |
132 |
for (handler <- handlers) server += handler |
|
133 |
server |
|
63823 | 134 |
} |
65079 | 135 |
|
136 |
||
65081 | 137 |
|
138 |
/** Isabelle resources **/ |
|
139 |
||
140 |
lazy val isabelle_resources: List[Handler] = |
|
65085 | 141 |
List(welcome, fonts()) |
65081 | 142 |
|
143 |
||
144 |
/* welcome */ |
|
145 |
||
65085 | 146 |
val welcome: Handler = |
66479 | 147 |
get("/", arg => |
148 |
if (arg.uri.toString == "/") { |
|
67865 | 149 |
val id = Isabelle_System.isabelle_id() |
65084 | 150 |
Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version)) |
65081 | 151 |
} |
152 |
else None) |
|
153 |
||
154 |
||
155 |
/* fonts */ |
|
65079 | 156 |
|
69363 | 157 |
private lazy val html_fonts: List[(String, Bytes)] = |
158 |
Isabelle_Fonts.fonts(html = true).map(entry => (entry.name -> entry.bytes)) |
|
65079 | 159 |
|
160 |
def fonts(root: String = "/fonts"): Handler = |
|
66479 | 161 |
get(root, arg => |
65079 | 162 |
{ |
66479 | 163 |
val uri_name = arg.uri.toString |
65086 | 164 |
if (uri_name == root) Some(Response.text(cat_lines(html_fonts.map(_._1)))) |
165 |
else html_fonts.collectFirst({ case (a, b) if uri_name == root + "/" + a => Response(b) }) |
|
65079 | 166 |
}) |
63823 | 167 |
} |