11 import java.nio.file.Files |
11 import java.nio.file.Files |
12 import java.net.{InetSocketAddress, URI, URL, HttpURLConnection} |
12 import java.net.{InetSocketAddress, URI, URL, HttpURLConnection} |
13 import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer} |
13 import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer} |
14 |
14 |
15 |
15 |
16 object HTTP |
16 object HTTP { |
17 { |
|
18 /** content **/ |
17 /** content **/ |
19 |
18 |
20 object Content |
19 object Content { |
21 { |
|
22 val mime_type_bytes: String = "application/octet-stream" |
20 val mime_type_bytes: String = "application/octet-stream" |
23 val mime_type_text: String = "text/plain; charset=utf-8" |
21 val mime_type_text: String = "text/plain; charset=utf-8" |
24 val mime_type_html: String = "text/html; charset=utf-8" |
22 val mime_type_html: String = "text/html; charset=utf-8" |
25 |
23 |
26 val default_mime_type: String = mime_type_bytes |
24 val default_mime_type: String = mime_type_bytes |
32 mime_type: String = default_mime_type, |
30 mime_type: String = default_mime_type, |
33 encoding: String = default_encoding, |
31 encoding: String = default_encoding, |
34 elapsed_time: Time = Time.zero): Content = |
32 elapsed_time: Time = Time.zero): Content = |
35 new Content(bytes, file_name, mime_type, encoding, elapsed_time) |
33 new Content(bytes, file_name, mime_type, encoding, elapsed_time) |
36 |
34 |
37 def read(file: JFile): Content = |
35 def read(file: JFile): Content = { |
38 { |
|
39 val bytes = Bytes.read(file) |
36 val bytes = Bytes.read(file) |
40 val file_name = file.getName |
37 val file_name = file.getName |
41 val mime_type = Option(Files.probeContentType(file.toPath)).getOrElse(default_mime_type) |
38 val mime_type = Option(Files.probeContentType(file.toPath)).getOrElse(default_mime_type) |
42 apply(bytes, file_name = file_name, mime_type = mime_type) |
39 apply(bytes, file_name = file_name, mime_type = mime_type) |
43 } |
40 } |
48 class Content private( |
45 class Content private( |
49 val bytes: Bytes, |
46 val bytes: Bytes, |
50 val file_name: String, |
47 val file_name: String, |
51 val mime_type: String, |
48 val mime_type: String, |
52 val encoding: String, |
49 val encoding: String, |
53 val elapsed_time: Time) |
50 val elapsed_time: Time |
54 { |
51 ) { |
55 def text: String = new String(bytes.array, encoding) |
52 def text: String = new String(bytes.array, encoding) |
56 def json: JSON.T = JSON.parse(text) |
53 def json: JSON.T = JSON.parse(text) |
57 } |
54 } |
58 |
55 |
59 |
56 |
60 |
57 |
61 /** client **/ |
58 /** client **/ |
62 |
59 |
63 val NEWLINE: String = "\r\n" |
60 val NEWLINE: String = "\r\n" |
64 |
61 |
65 object Client |
62 object Client { |
66 { |
|
67 val default_timeout: Time = Time.seconds(180) |
63 val default_timeout: Time = Time.seconds(180) |
68 |
64 |
69 def open_connection(url: URL, |
65 def open_connection( |
|
66 url: URL, |
70 timeout: Time = default_timeout, |
67 timeout: Time = default_timeout, |
71 user_agent: String = ""): HttpURLConnection = |
68 user_agent: String = "" |
72 { |
69 ): HttpURLConnection = { |
73 url.openConnection match { |
70 url.openConnection match { |
74 case connection: HttpURLConnection => |
71 case connection: HttpURLConnection => |
75 if (0 < timeout.ms && timeout.ms <= Integer.MAX_VALUE) { |
72 if (0 < timeout.ms && timeout.ms <= Integer.MAX_VALUE) { |
76 val ms = timeout.ms.toInt |
73 val ms = timeout.ms.toInt |
77 connection.setConnectTimeout(ms) |
74 connection.setConnectTimeout(ms) |
81 connection |
78 connection |
82 case _ => error("Bad URL (not HTTP): " + quote(url.toString)) |
79 case _ => error("Bad URL (not HTTP): " + quote(url.toString)) |
83 } |
80 } |
84 } |
81 } |
85 |
82 |
86 def get_content(connection: HttpURLConnection): Content = |
83 def get_content(connection: HttpURLConnection): Content = { |
87 { |
|
88 val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r |
84 val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r |
89 |
85 |
90 val start = Time.now() |
86 val start = Time.now() |
91 using(connection.getInputStream)(stream => |
87 using(connection.getInputStream)(stream => { |
92 { |
|
93 val bytes = Bytes.read_stream(stream, hint = connection.getContentLength) |
88 val bytes = Bytes.read_stream(stream, hint = connection.getContentLength) |
94 val stop = Time.now() |
89 val stop = Time.now() |
95 |
90 |
96 val file_name = Url.file_name(connection.getURL) |
91 val file_name = Url.file_name(connection.getURL) |
97 val mime_type = Option(connection.getContentType).getOrElse(Content.default_mime_type) |
92 val mime_type = Option(connection.getContentType).getOrElse(Content.default_mime_type) |
107 } |
102 } |
108 |
103 |
109 def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content = |
104 def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content = |
110 get_content(open_connection(url, timeout = timeout, user_agent = user_agent)) |
105 get_content(open_connection(url, timeout = timeout, user_agent = user_agent)) |
111 |
106 |
112 def post(url: URL, parameters: List[(String, Any)], |
107 def post( |
|
108 url: URL, |
|
109 parameters: List[(String, Any)], |
113 timeout: Time = default_timeout, |
110 timeout: Time = default_timeout, |
114 user_agent: String = ""): Content = |
111 user_agent: String = "" |
115 { |
112 ): Content = { |
116 val connection = open_connection(url, timeout = timeout, user_agent = user_agent) |
113 val connection = open_connection(url, timeout = timeout, user_agent = user_agent) |
117 connection.setRequestMethod("POST") |
114 connection.setRequestMethod("POST") |
118 connection.setDoOutput(true) |
115 connection.setDoOutput(true) |
119 |
116 |
120 val boundary = UUID.random().toString |
117 val boundary = UUID.random().toString |
121 connection.setRequestProperty( |
118 connection.setRequestProperty( |
122 "Content-Type", "multipart/form-data; boundary=" + quote(boundary)) |
119 "Content-Type", "multipart/form-data; boundary=" + quote(boundary)) |
123 |
120 |
124 using(connection.getOutputStream)(out => |
121 using(connection.getOutputStream)(out => { |
125 { |
|
126 def output(s: String): Unit = out.write(UTF8.bytes(s)) |
122 def output(s: String): Unit = out.write(UTF8.bytes(s)) |
127 def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE)) |
123 def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE)) |
128 def output_boundary(end: Boolean = false): Unit = |
124 def output_boundary(end: Boolean = false): Unit = |
129 output("--" + boundary + (if (end) "--" else "") + NEWLINE) |
125 output("--" + boundary + (if (end) "--" else "") + NEWLINE) |
130 def output_name(name: String): Unit = |
126 def output_name(name: String): Unit = |
131 output("Content-Disposition: form-data; name=" + quote(name)) |
127 output("Content-Disposition: form-data; name=" + quote(name)) |
132 def output_value(value: Any): Unit = |
128 def output_value(value: Any): Unit = { |
133 { |
|
134 output_newline(2) |
129 output_newline(2) |
135 output(value.toString) |
130 output(value.toString) |
136 } |
131 } |
137 def output_content(content: Content): Unit = |
132 def output_content(content: Content): Unit = { |
138 { |
|
139 proper_string(content.file_name).foreach(s => output("; filename=" + quote(s))) |
133 proper_string(content.file_name).foreach(s => output("; filename=" + quote(s))) |
140 output_newline() |
134 output_newline() |
141 proper_string(content.mime_type).foreach(s => output("Content-Type: " + s)) |
135 proper_string(content.mime_type).foreach(s => output("Content-Type: " + s)) |
142 output_newline(2) |
136 output_newline(2) |
143 content.bytes.write_stream(out) |
137 content.bytes.write_stream(out) |
175 |
169 |
176 class Request private[HTTP]( |
170 class Request private[HTTP]( |
177 val server_name: String, |
171 val server_name: String, |
178 val service_name: String, |
172 val service_name: String, |
179 val uri: URI, |
173 val uri: URI, |
180 val input: Bytes) |
174 val input: Bytes |
181 { |
175 ) { |
182 def home: String = url_path(server_name, service_name) |
176 def home: String = url_path(server_name, service_name) |
183 def root: String = home + "/" |
177 def root: String = home + "/" |
184 def query: String = home + "?" |
178 def query: String = home + "?" |
185 |
179 |
186 def toplevel: Boolean = uri_name == home || uri_name == root |
180 def toplevel: Boolean = uri_name == home || uri_name == root |
222 def content(content: Content): Response = apply(content.bytes, content.mime_type) |
215 def content(content: Content): Response = apply(content.bytes, content.mime_type) |
223 def read(file: JFile): Response = content(Content.read(file)) |
216 def read(file: JFile): Response = content(Content.read(file)) |
224 def read(path: Path): Response = content(Content.read(path)) |
217 def read(path: Path): Response = content(Content.read(path)) |
225 } |
218 } |
226 |
219 |
227 class Response private[HTTP](val output: Bytes, val content_type: String) |
220 class Response private[HTTP](val output: Bytes, val content_type: String) { |
228 { |
|
229 override def toString: String = output.toString |
221 override def toString: String = output.toString |
230 |
222 |
231 def write(http: HttpExchange, code: Int): Unit = |
223 def write(http: HttpExchange, code: Int): Unit = { |
232 { |
|
233 http.getResponseHeaders.set("Content-Type", content_type) |
224 http.getResponseHeaders.set("Content-Type", content_type) |
234 http.sendResponseHeaders(code, output.length.toLong) |
225 http.sendResponseHeaders(code, output.length.toLong) |
235 using(http.getResponseBody)(output.write_stream) |
226 using(http.getResponseBody)(output.write_stream) |
236 } |
227 } |
237 } |
228 } |
238 |
229 |
239 |
230 |
240 /* service */ |
231 /* service */ |
241 |
232 |
242 abstract class Service(val name: String, method: String = "GET") |
233 abstract class Service(val name: String, method: String = "GET") { |
243 { |
|
244 override def toString: String = name |
234 override def toString: String = name |
245 |
235 |
246 def apply(request: Request): Option[Response] |
236 def apply(request: Request): Option[Response] |
247 |
237 |
248 def context(server_name: String): String = |
238 def context(server_name: String): String = |
286 override def toString: String = url |
275 override def toString: String = url |
287 } |
276 } |
288 |
277 |
289 def server( |
278 def server( |
290 name: String = UUID.random().toString, |
279 name: String = UUID.random().toString, |
291 services: List[Service] = isabelle_services): Server = |
280 services: List[Service] = isabelle_services |
292 { |
281 ): Server = { |
293 val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0) |
282 val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0) |
294 http_server.setExecutor(null) |
283 http_server.setExecutor(null) |
295 |
284 |
296 val server = new Server(name, http_server) |
285 val server = new Server(name, http_server) |
297 for (service <- services) server += service |
286 for (service <- services) server += service |
344 |
331 |
345 /* pdfjs */ |
332 /* pdfjs */ |
346 |
333 |
347 object PDFjs_Service extends PDFjs() |
334 object PDFjs_Service extends PDFjs() |
348 |
335 |
349 class PDFjs(name: String = "pdfjs") extends Service(name) |
336 class PDFjs(name: String = "pdfjs") extends Service(name) { |
350 { |
|
351 def apply(request: Request): Option[Response] = |
337 def apply(request: Request): Option[Response] = |
352 for { |
338 for { |
353 p <- request.uri_path |
339 p <- request.uri_path |
354 path = Path.explode("$ISABELLE_PDFJS_HOME") + p if path.is_file |
340 path = Path.explode("$ISABELLE_PDFJS_HOME") + p if path.is_file |
355 s = p.implode if s.startsWith("build/") || s.startsWith("web/") |
341 s = p.implode if s.startsWith("build/") || s.startsWith("web/") |