author | wenzelm |
Mon, 15 Mar 2021 11:43:56 +0100 | |
changeset 73440 | 3696bb4085ed |
parent 73439 | cb127ce2c092 |
child 73518 | c42144d9dde6 |
permissions | -rw-r--r-- |
65077 | 1 |
/* Title: Pure/General/http.scala |
63823 | 2 |
Author: Makarius |
3 |
||
73438 | 4 |
HTTP client and server support. |
63823 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
73417 | 10 |
import java.io.{File => JFile} |
11 |
import java.net.{InetSocketAddress, URI, URL, URLConnection, HttpURLConnection} |
|
63823 | 12 |
import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer} |
13 |
||
14 |
||
65077 | 15 |
object HTTP |
63823 | 16 |
{ |
73416
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
17 |
/** content **/ |
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
18 |
|
73417 | 19 |
val mime_type_bytes: String = "application/octet-stream" |
20 |
val mime_type_text: String = "text/plain; charset=utf-8" |
|
21 |
val mime_type_html: String = "text/html; charset=utf-8" |
|
22 |
||
23 |
val default_mime_type: String = mime_type_bytes |
|
24 |
val default_encoding: String = UTF8.charset_name |
|
73416
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
25 |
|
73417 | 26 |
sealed case class Content( |
27 |
bytes: Bytes, |
|
28 |
file_name: String = "", |
|
29 |
mime_type: String = default_mime_type, |
|
73429
8970081c6500
elapsed time to download content (and for the server to provide content);
wenzelm
parents:
73425
diff
changeset
|
30 |
encoding: String = default_encoding, |
8970081c6500
elapsed time to download content (and for the server to provide content);
wenzelm
parents:
73425
diff
changeset
|
31 |
elapsed_time: Time = Time.zero) |
73416
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
32 |
{ |
73440 | 33 |
def text: String = new String(bytes.array, encoding) |
73416
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
34 |
} |
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
35 |
|
73417 | 36 |
def read_content(file: JFile): Content = |
37 |
{ |
|
38 |
val bytes = Bytes.read(file) |
|
39 |
val file_name = file.getName |
|
40 |
val mime_type = |
|
41 |
Option(URLConnection.guessContentTypeFromName(file_name)).getOrElse(default_mime_type) |
|
42 |
Content(bytes, file_name = file_name, mime_type = mime_type) |
|
43 |
} |
|
44 |
||
45 |
def read_content(path: Path): Content = read_content(path.file) |
|
46 |
||
73416
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
47 |
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
48 |
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
49 |
/** client **/ |
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
50 |
|
73417 | 51 |
val NEWLINE: String = "\r\n" |
52 |
||
73416
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
53 |
object Client |
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
54 |
{ |
73439 | 55 |
val default_timeout: Time = Time.seconds(180) |
73422 | 56 |
|
57 |
def open_connection(url: URL, |
|
58 |
timeout: Time = default_timeout, |
|
59 |
user_agent: String = ""): HttpURLConnection = |
|
73421 | 60 |
{ |
61 |
url.openConnection match { |
|
62 |
case connection: HttpURLConnection => |
|
73422 | 63 |
if (0 < timeout.ms && timeout.ms <= Integer.MAX_VALUE) { |
64 |
val ms = timeout.ms.toInt |
|
65 |
connection.setConnectTimeout(ms) |
|
66 |
connection.setReadTimeout(ms) |
|
67 |
} |
|
73421 | 68 |
proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s)) |
69 |
connection |
|
70 |
case _ => error("Bad URL (not HTTP): " + quote(url.toString)) |
|
71 |
} |
|
72 |
} |
|
73417 | 73 |
|
73421 | 74 |
def get_content(connection: HttpURLConnection): Content = |
73417 | 75 |
{ |
76 |
val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r |
|
73429
8970081c6500
elapsed time to download content (and for the server to provide content);
wenzelm
parents:
73425
diff
changeset
|
77 |
|
8970081c6500
elapsed time to download content (and for the server to provide content);
wenzelm
parents:
73425
diff
changeset
|
78 |
val start = Time.now() |
73417 | 79 |
using(connection.getInputStream)(stream => |
80 |
{ |
|
81 |
val bytes = Bytes.read_stream(stream, hint = connection.getContentLength) |
|
73429
8970081c6500
elapsed time to download content (and for the server to provide content);
wenzelm
parents:
73425
diff
changeset
|
82 |
val stop = Time.now() |
8970081c6500
elapsed time to download content (and for the server to provide content);
wenzelm
parents:
73425
diff
changeset
|
83 |
|
73417 | 84 |
val file_name = Url.file_name(connection.getURL) |
85 |
val mime_type = Option(connection.getContentType).getOrElse(default_mime_type) |
|
86 |
val encoding = |
|
87 |
(connection.getContentEncoding, mime_type) match { |
|
88 |
case (enc, _) if enc != null => enc |
|
89 |
case (_, Charset(enc)) => enc |
|
90 |
case _ => default_encoding |
|
91 |
} |
|
73429
8970081c6500
elapsed time to download content (and for the server to provide content);
wenzelm
parents:
73425
diff
changeset
|
92 |
Content(bytes, file_name = file_name, mime_type = mime_type, |
8970081c6500
elapsed time to download content (and for the server to provide content);
wenzelm
parents:
73425
diff
changeset
|
93 |
encoding = encoding, elapsed_time = stop - start) |
73417 | 94 |
}) |
95 |
} |
|
96 |
||
73422 | 97 |
def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content = |
98 |
get_content(open_connection(url, timeout = timeout, user_agent = user_agent)) |
|
73417 | 99 |
|
73422 | 100 |
def post(url: URL, parameters: List[(String, Any)], |
101 |
timeout: Time = default_timeout, |
|
102 |
user_agent: String = ""): Content = |
|
73416
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
103 |
{ |
73422 | 104 |
val connection = open_connection(url, timeout = timeout, user_agent = user_agent) |
73421 | 105 |
connection.setRequestMethod("POST") |
106 |
connection.setDoOutput(true) |
|
73417 | 107 |
|
73421 | 108 |
val boundary = UUID.random_string() |
109 |
connection.setRequestProperty( |
|
110 |
"Content-Type", "multipart/form-data; boundary=" + quote(boundary)) |
|
73417 | 111 |
|
73421 | 112 |
using(connection.getOutputStream)(out => |
113 |
{ |
|
114 |
def output(s: String): Unit = out.write(UTF8.bytes(s)) |
|
115 |
def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE)) |
|
116 |
def output_boundary(end: Boolean = false): Unit = |
|
117 |
output("--" + boundary + (if (end) "--" else "") + NEWLINE) |
|
118 |
def output_name(name: String): Unit = |
|
119 |
output("Content-Disposition: form-data; name=" + quote(name)) |
|
120 |
def output_value(value: Any): Unit = |
|
121 |
{ |
|
122 |
output_newline(2) |
|
123 |
output(value.toString) |
|
124 |
} |
|
125 |
def output_content(content: Content): Unit = |
|
126 |
{ |
|
127 |
proper_string(content.file_name).foreach(s => output("; filename=" + quote(s))) |
|
128 |
output_newline() |
|
129 |
proper_string(content.mime_type).foreach(s => output("Content-Type: " + s)) |
|
130 |
output_newline(2) |
|
131 |
content.bytes.write_stream(out) |
|
132 |
} |
|
73417 | 133 |
|
73421 | 134 |
output_newline(2) |
73417 | 135 |
|
73421 | 136 |
for { (name, value) <- parameters } { |
137 |
output_boundary() |
|
138 |
output_name(name) |
|
139 |
value match { |
|
140 |
case content: Content => output_content(content) |
|
141 |
case file: JFile => output_content(read_content(file)) |
|
142 |
case path: Path => output_content(read_content(path)) |
|
143 |
case _ => output_value(value) |
|
144 |
} |
|
145 |
output_newline() |
|
146 |
} |
|
147 |
output_boundary(end = true) |
|
148 |
out.flush() |
|
149 |
}) |
|
73417 | 150 |
|
73421 | 151 |
get_content(connection) |
73416
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
152 |
} |
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
153 |
} |
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
154 |
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
155 |
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
156 |
|
65081 | 157 |
/** server **/ |
158 |
||
65078 | 159 |
/* response */ |
160 |
||
161 |
object Response |
|
162 |
{ |
|
163 |
def apply( |
|
164 |
bytes: Bytes = Bytes.empty, |
|
73417 | 165 |
content_type: String = mime_type_bytes): Response = |
65078 | 166 |
new Response(bytes, content_type) |
167 |
||
168 |
val empty: Response = apply() |
|
73417 | 169 |
def text(s: String): Response = apply(Bytes(s), mime_type_text) |
170 |
def html(s: String): Response = apply(Bytes(s), mime_type_html) |
|
65078 | 171 |
} |
172 |
||
173 |
class Response private[HTTP](val bytes: Bytes, val content_type: String) |
|
174 |
{ |
|
175 |
override def toString: String = bytes.toString |
|
176 |
} |
|
177 |
||
178 |
||
179 |
/* exchange */ |
|
180 |
||
181 |
class Exchange private[HTTP](val http_exchange: HttpExchange) |
|
182 |
{ |
|
183 |
def request_method: String = http_exchange.getRequestMethod |
|
184 |
def request_uri: URI = http_exchange.getRequestURI |
|
185 |
||
186 |
def read_request(): Bytes = |
|
69393
ed0824ef337e
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents:
69374
diff
changeset
|
187 |
using(http_exchange.getRequestBody)(Bytes.read_stream(_)) |
65078 | 188 |
|
73340 | 189 |
def write_response(code: Int, response: Response): Unit = |
65078 | 190 |
{ |
73439 | 191 |
http_exchange.getResponseHeaders.set("Content-Type", response.content_type) |
65078 | 192 |
http_exchange.sendResponseHeaders(code, response.bytes.length.toLong) |
73439 | 193 |
using(http_exchange.getResponseBody)(response.bytes.write_stream) |
65078 | 194 |
} |
195 |
} |
|
196 |
||
197 |
||
73413 | 198 |
/* handler for request method */ |
66207 | 199 |
|
200 |
sealed case class Arg(method: String, uri: URI, request: Bytes) |
|
201 |
{ |
|
202 |
def decode_properties: Properties.T = |
|
66923 | 203 |
space_explode('&', request.text).map(s => |
204 |
space_explode('=', s) match { |
|
67245 | 205 |
case List(a, b) => Url.decode(a) -> Url.decode(b) |
66207 | 206 |
case _ => error("Malformed key-value pair in HTTP/POST: " + quote(s)) |
207 |
}) |
|
208 |
} |
|
209 |
||
73413 | 210 |
object Handler |
211 |
{ |
|
212 |
def apply(root: String, body: Exchange => Unit): Handler = |
|
73439 | 213 |
new Handler(root, (x: HttpExchange) => body(new Exchange(x))) |
73413 | 214 |
|
215 |
def method(name: String, root: String, body: Arg => Option[Response]): Handler = |
|
216 |
apply(root, http => |
|
217 |
{ |
|
218 |
val request = http.read_request() |
|
219 |
if (http.request_method == name) { |
|
220 |
val arg = Arg(name, http.request_uri, request) |
|
221 |
Exn.capture(body(arg)) match { |
|
222 |
case Exn.Res(Some(response)) => |
|
223 |
http.write_response(200, response) |
|
224 |
case Exn.Res(None) => |
|
225 |
http.write_response(404, Response.empty) |
|
226 |
case Exn.Exn(ERROR(msg)) => |
|
227 |
http.write_response(500, Response.text(Output.error_message_text(msg))) |
|
228 |
case Exn.Exn(exn) => throw exn |
|
229 |
} |
|
65078 | 230 |
} |
73413 | 231 |
else http.write_response(400, Response.empty) |
232 |
}) |
|
65076 | 233 |
|
73413 | 234 |
def get(root: String, body: Arg => Option[Response]): Handler = method("GET", root, body) |
235 |
def post(root: String, body: Arg => Option[Response]): Handler = method("POST", root, body) |
|
236 |
} |
|
237 |
||
238 |
class Handler private(val root: String, val handler: HttpHandler) |
|
239 |
{ |
|
240 |
override def toString: String = root |
|
241 |
} |
|
66207 | 242 |
|
65077 | 243 |
|
244 |
/* server */ |
|
245 |
||
246 |
class Server private[HTTP](val http_server: HttpServer) |
|
247 |
{ |
|
73340 | 248 |
def += (handler: Handler): Unit = http_server.createContext(handler.root, handler.handler) |
249 |
def -= (handler: Handler): Unit = http_server.removeContext(handler.root) |
|
65077 | 250 |
|
73439 | 251 |
def start(): Unit = http_server.start() |
73367 | 252 |
def stop(): Unit = http_server.stop(0) |
65077 | 253 |
|
254 |
def address: InetSocketAddress = http_server.getAddress |
|
255 |
def url: String = "http://" + address.getHostName + ":" + address.getPort |
|
256 |
override def toString: String = url |
|
257 |
} |
|
258 |
||
65081 | 259 |
def server(handlers: List[Handler] = isabelle_resources): Server = |
63823 | 260 |
{ |
69463 | 261 |
val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0) |
65077 | 262 |
http_server.setExecutor(null) |
65076 | 263 |
|
65077 | 264 |
val server = new Server(http_server) |
265 |
for (handler <- handlers) server += handler |
|
266 |
server |
|
63823 | 267 |
} |
65079 | 268 |
|
269 |
||
65081 | 270 |
|
271 |
/** Isabelle resources **/ |
|
272 |
||
273 |
lazy val isabelle_resources: List[Handler] = |
|
65085 | 274 |
List(welcome, fonts()) |
65081 | 275 |
|
276 |
||
277 |
/* welcome */ |
|
278 |
||
65085 | 279 |
val welcome: Handler = |
73413 | 280 |
Handler.get("/", arg => |
66479 | 281 |
if (arg.uri.toString == "/") { |
67865 | 282 |
val id = Isabelle_System.isabelle_id() |
65084 | 283 |
Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version)) |
65081 | 284 |
} |
285 |
else None) |
|
286 |
||
287 |
||
288 |
/* fonts */ |
|
65079 | 289 |
|
69374 | 290 |
private lazy val html_fonts: List[Isabelle_Fonts.Entry] = |
291 |
Isabelle_Fonts.fonts(hidden = true) |
|
65079 | 292 |
|
293 |
def fonts(root: String = "/fonts"): Handler = |
|
73413 | 294 |
Handler.get(root, arg => |
65079 | 295 |
{ |
66479 | 296 |
val uri_name = arg.uri.toString |
69364
91dbade9a5fa
proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents:
69363
diff
changeset
|
297 |
if (uri_name == root) { |
69366 | 298 |
Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name)))) |
69364
91dbade9a5fa
proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents:
69363
diff
changeset
|
299 |
} |
91dbade9a5fa
proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents:
69363
diff
changeset
|
300 |
else { |
91dbade9a5fa
proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents:
69363
diff
changeset
|
301 |
html_fonts.collectFirst( |
69366 | 302 |
{ case entry if uri_name == root + "/" + entry.path.file_name => Response(entry.bytes) }) |
69364
91dbade9a5fa
proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents:
69363
diff
changeset
|
303 |
} |
65079 | 304 |
}) |
63823 | 305 |
} |