| author | wenzelm |
| Wed, 12 Feb 2025 00:53:15 +0100 | |
| changeset 82143 | a43e39c52f26 |
| parent 82107 | 6c3b7d1f2115 |
| child 82134 | 5d57110da8eb |
| child 82153 | 3c2451d482bd |
| permissions | -rw-r--r-- |
| 65077 | 1 |
/* Title: Pure/General/http.scala |
| 63823 | 2 |
Author: Makarius |
| 81781 | 3 |
Author: Fabian Huch, TU München |
| 63823 | 4 |
|
| 73438 | 5 |
HTTP client and server support. |
| 63823 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
| 73417 | 11 |
import java.io.{File => JFile}
|
| 75104 | 12 |
import java.nio.file.Files |
| 79658 | 13 |
import java.net.{InetSocketAddress, URI, HttpURLConnection}
|
|
80243
b2889dd54a2a
use Content-Digest header in HEAD requests instead of length (to track non-monotone changes);
Fabian Huch <huch@in.tum.de>
parents:
80202
diff
changeset
|
14 |
import java.util.HexFormat |
| 63823 | 15 |
import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
|
16 |
||
17 |
||
| 75393 | 18 |
object HTTP {
|
|
73416
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
19 |
/** content **/ |
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
20 |
|
| 75393 | 21 |
object Content {
|
| 75106 | 22 |
val mime_type_bytes: String = "application/octet-stream" |
23 |
val mime_type_text: String = "text/plain; charset=utf-8" |
|
24 |
val mime_type_html: String = "text/html; charset=utf-8" |
|
| 82106 | 25 |
val mime_type_css: String = "text/css; charset=utf-8" |
26 |
val mime_type_js: String = "text/javascript; charset=utf-8" |
|
| 73417 | 27 |
|
| 75106 | 28 |
val default_mime_type: String = mime_type_bytes |
| 76356 | 29 |
val default_encoding: String = UTF8.charset.name |
| 75106 | 30 |
|
31 |
def apply( |
|
32 |
bytes: Bytes, |
|
33 |
file_name: String = "", |
|
34 |
mime_type: String = default_mime_type, |
|
35 |
encoding: String = default_encoding, |
|
36 |
elapsed_time: Time = Time.zero): Content = |
|
37 |
new Content(bytes, file_name, mime_type, encoding, elapsed_time) |
|
|
73416
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
38 |
|
| 75393 | 39 |
def read(file: JFile): Content = {
|
| 75106 | 40 |
val bytes = Bytes.read(file) |
41 |
val file_name = file.getName |
|
42 |
val mime_type = Option(Files.probeContentType(file.toPath)).getOrElse(default_mime_type) |
|
43 |
apply(bytes, file_name = file_name, mime_type = mime_type) |
|
44 |
} |
|
45 |
||
46 |
def read(path: Path): Content = read(path.file) |
|
47 |
} |
|
48 |
||
49 |
class Content private( |
|
50 |
val bytes: Bytes, |
|
51 |
val file_name: String, |
|
52 |
val mime_type: String, |
|
53 |
val encoding: String, |
|
| 75393 | 54 |
val elapsed_time: Time |
55 |
) {
|
|
| 80368 | 56 |
def text: String = new String(bytes.make_array, encoding) |
| 74945 | 57 |
def json: JSON.T = JSON.parse(text) |
|
73416
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
58 |
} |
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
59 |
|
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
60 |
|
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
61 |
|
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
62 |
/** client **/ |
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
63 |
|
| 73417 | 64 |
val NEWLINE: String = "\r\n" |
65 |
||
| 75393 | 66 |
object Client {
|
| 73439 | 67 |
val default_timeout: Time = Time.seconds(180) |
| 73422 | 68 |
|
| 75393 | 69 |
def open_connection( |
|
79510
d8330439823a
clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
wenzelm
parents:
78768
diff
changeset
|
70 |
url: Url, |
| 73422 | 71 |
timeout: Time = default_timeout, |
| 75393 | 72 |
user_agent: String = "" |
73 |
): HttpURLConnection = {
|
|
|
79510
d8330439823a
clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
wenzelm
parents:
78768
diff
changeset
|
74 |
url.open_connection() match {
|
| 73421 | 75 |
case connection: HttpURLConnection => |
| 78243 | 76 |
if (0 < timeout.ms && timeout.ms <= Int.MaxValue) {
|
| 73422 | 77 |
val ms = timeout.ms.toInt |
78 |
connection.setConnectTimeout(ms) |
|
79 |
connection.setReadTimeout(ms) |
|
80 |
} |
|
| 73421 | 81 |
proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s))
|
82 |
connection |
|
83 |
case _ => error("Bad URL (not HTTP): " + quote(url.toString))
|
|
84 |
} |
|
85 |
} |
|
| 73417 | 86 |
|
| 75393 | 87 |
def get_content(connection: HttpURLConnection): Content = {
|
| 73417 | 88 |
val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r |
|
73429
8970081c6500
elapsed time to download content (and for the server to provide content);
wenzelm
parents:
73425
diff
changeset
|
89 |
|
|
8970081c6500
elapsed time to download content (and for the server to provide content);
wenzelm
parents:
73425
diff
changeset
|
90 |
val start = Time.now() |
| 75394 | 91 |
using(connection.getInputStream) { stream =>
|
| 73417 | 92 |
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
|
93 |
val stop = Time.now() |
|
8970081c6500
elapsed time to download content (and for the server to provide content);
wenzelm
parents:
73425
diff
changeset
|
94 |
|
|
79510
d8330439823a
clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
wenzelm
parents:
78768
diff
changeset
|
95 |
val file_name = Url.file_name(Url(connection.getURL.toURI)) |
| 75106 | 96 |
val mime_type = Option(connection.getContentType).getOrElse(Content.default_mime_type) |
| 73417 | 97 |
val encoding = |
98 |
(connection.getContentEncoding, mime_type) match {
|
|
99 |
case (enc, _) if enc != null => enc |
|
100 |
case (_, Charset(enc)) => enc |
|
| 75106 | 101 |
case _ => Content.default_encoding |
| 73417 | 102 |
} |
|
73429
8970081c6500
elapsed time to download content (and for the server to provide content);
wenzelm
parents:
73425
diff
changeset
|
103 |
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
|
104 |
encoding = encoding, elapsed_time = stop - start) |
| 75394 | 105 |
} |
| 73417 | 106 |
} |
107 |
||
|
79510
d8330439823a
clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
wenzelm
parents:
78768
diff
changeset
|
108 |
def get(url: Url, timeout: Time = default_timeout, user_agent: String = ""): Content = |
| 73422 | 109 |
get_content(open_connection(url, timeout = timeout, user_agent = user_agent)) |
| 73417 | 110 |
|
| 75393 | 111 |
def post( |
|
79510
d8330439823a
clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
wenzelm
parents:
78768
diff
changeset
|
112 |
url: Url, |
| 75393 | 113 |
parameters: List[(String, Any)], |
| 73422 | 114 |
timeout: Time = default_timeout, |
| 75393 | 115 |
user_agent: String = "" |
116 |
): Content = {
|
|
| 73422 | 117 |
val connection = open_connection(url, timeout = timeout, user_agent = user_agent) |
| 73421 | 118 |
connection.setRequestMethod("POST")
|
119 |
connection.setDoOutput(true) |
|
| 73417 | 120 |
|
| 79717 | 121 |
val boundary = UUID.random_string() |
| 73421 | 122 |
connection.setRequestProperty( |
123 |
"Content-Type", "multipart/form-data; boundary=" + quote(boundary)) |
|
| 73417 | 124 |
|
| 75394 | 125 |
using(connection.getOutputStream) { out =>
|
| 73421 | 126 |
def output(s: String): Unit = out.write(UTF8.bytes(s)) |
127 |
def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE)) |
|
128 |
def output_boundary(end: Boolean = false): Unit = |
|
129 |
output("--" + boundary + (if (end) "--" else "") + NEWLINE)
|
|
130 |
def output_name(name: String): Unit = |
|
131 |
output("Content-Disposition: form-data; name=" + quote(name))
|
|
| 75393 | 132 |
def output_value(value: Any): Unit = {
|
| 73421 | 133 |
output_newline(2) |
134 |
output(value.toString) |
|
135 |
} |
|
| 75393 | 136 |
def output_content(content: Content): Unit = {
|
| 73421 | 137 |
proper_string(content.file_name).foreach(s => output("; filename=" + quote(s)))
|
138 |
output_newline() |
|
139 |
proper_string(content.mime_type).foreach(s => output("Content-Type: " + s))
|
|
140 |
output_newline(2) |
|
141 |
content.bytes.write_stream(out) |
|
142 |
} |
|
| 73417 | 143 |
|
| 73421 | 144 |
output_newline(2) |
| 73417 | 145 |
|
| 73421 | 146 |
for { (name, value) <- parameters } {
|
147 |
output_boundary() |
|
148 |
output_name(name) |
|
149 |
value match {
|
|
150 |
case content: Content => output_content(content) |
|
| 75106 | 151 |
case file: JFile => output_content(Content.read(file)) |
152 |
case path: Path => output_content(Content.read(path)) |
|
| 73421 | 153 |
case _ => output_value(value) |
154 |
} |
|
155 |
output_newline() |
|
156 |
} |
|
157 |
output_boundary(end = true) |
|
158 |
out.flush() |
|
| 75394 | 159 |
} |
| 73417 | 160 |
|
| 73421 | 161 |
get_content(connection) |
|
73416
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
162 |
} |
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
163 |
} |
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
164 |
|
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
165 |
|
|
08aa4c1ed579
clarified signature: more explicit HTTP operations;
wenzelm
parents:
73413
diff
changeset
|
166 |
|
| 65081 | 167 |
/** server **/ |
168 |
||
| 75107 | 169 |
/* request */ |
170 |
||
| 75108 | 171 |
def url_path(names: String*): String = |
172 |
names.iterator.flatMap(a => if (a.isEmpty) None else Some("/" + a)).mkString
|
|
173 |
||
174 |
class Request private[HTTP]( |
|
| 75146 | 175 |
val server_name: String, |
176 |
val service_name: String, |
|
| 75108 | 177 |
val uri: URI, |
| 75393 | 178 |
val input: Bytes |
179 |
) {
|
|
| 75146 | 180 |
def home: String = url_path(server_name, service_name) |
| 75107 | 181 |
def root: String = home + "/" |
182 |
def query: String = home + "?" |
|
183 |
||
| 75109 | 184 |
def toplevel: Boolean = uri_name == home || uri_name == root |
185 |
||
186 |
val uri_name: String = uri.toString |
|
| 75107 | 187 |
|
188 |
def uri_path: Option[Path] = |
|
189 |
for {
|
|
| 75111 | 190 |
s <- Option(uri.getPath).flatMap(Library.try_unprefix(root, _)) |
191 |
if Path.is_wellformed(s) |
|
192 |
p = Path.explode(s) if p.all_basic |
|
| 75107 | 193 |
} yield p |
194 |
||
| 75112 | 195 |
def decode_query: Option[String] = |
196 |
Library.try_unprefix(query, uri_name).map(Url.decode) |
|
197 |
||
| 75107 | 198 |
def decode_properties: Properties.T = |
199 |
space_explode('&', input.text).map(
|
|
200 |
{
|
|
201 |
case Properties.Eq(a, b) => Url.decode(a) -> Url.decode(b) |
|
202 |
case s => error("Malformed key-value pair in HTTP/POST: " + quote(s))
|
|
203 |
}) |
|
204 |
} |
|
205 |
||
206 |
||
| 65078 | 207 |
/* response */ |
208 |
||
| 75393 | 209 |
object Response {
|
| 65078 | 210 |
def apply( |
211 |
bytes: Bytes = Bytes.empty, |
|
| 75106 | 212 |
content_type: String = Content.mime_type_bytes): Response = |
| 65078 | 213 |
new Response(bytes, content_type) |
214 |
||
215 |
val empty: Response = apply() |
|
| 75106 | 216 |
def text(s: String): Response = apply(Bytes(s), Content.mime_type_text) |
217 |
def html(s: String): Response = apply(Bytes(s), Content.mime_type_html) |
|
|
75105
03115c9eea00
support for PDF.js: platform-independent PDF viewer;
wenzelm
parents:
75104
diff
changeset
|
218 |
|
|
03115c9eea00
support for PDF.js: platform-independent PDF viewer;
wenzelm
parents:
75104
diff
changeset
|
219 |
def content(content: Content): Response = apply(content.bytes, content.mime_type) |
| 75106 | 220 |
def read(file: JFile): Response = content(Content.read(file)) |
221 |
def read(path: Path): Response = content(Content.read(path)) |
|
| 65078 | 222 |
} |
223 |
||
| 75393 | 224 |
class Response private[HTTP](val output: Bytes, val content_type: String) {
|
| 75107 | 225 |
override def toString: String = output.toString |
| 65078 | 226 |
|
|
80201
6ac48d53d371
add HEAD to http server: should send same header fields as if request was GET;
Fabian Huch <huch@in.tum.de>
parents:
79717
diff
changeset
|
227 |
def write(http: HttpExchange, code: Int, is_head: Boolean = false): Unit = {
|
| 75107 | 228 |
http.getResponseHeaders.set("Content-Type", content_type)
|
|
80243
b2889dd54a2a
use Content-Digest header in HEAD requests instead of length (to track non-monotone changes);
Fabian Huch <huch@in.tum.de>
parents:
80202
diff
changeset
|
229 |
if (is_head) {
|
|
b2889dd54a2a
use Content-Digest header in HEAD requests instead of length (to track non-monotone changes);
Fabian Huch <huch@in.tum.de>
parents:
80202
diff
changeset
|
230 |
val encoded_digest = Base64.encode(HexFormat.of().parseHex(SHA1.digest(output).toString)) |
|
b2889dd54a2a
use Content-Digest header in HEAD requests instead of length (to track non-monotone changes);
Fabian Huch <huch@in.tum.de>
parents:
80202
diff
changeset
|
231 |
http.getResponseHeaders.set("Content-Digest", "sha=:" + encoded_digest + ":")
|
|
b2889dd54a2a
use Content-Digest header in HEAD requests instead of length (to track non-monotone changes);
Fabian Huch <huch@in.tum.de>
parents:
80202
diff
changeset
|
232 |
} |
|
80357
fe123d033e76
clarified signature: pro-forma support for Bytes with size: Long;
wenzelm
parents:
80243
diff
changeset
|
233 |
http.sendResponseHeaders(code, if (is_head) -1 else output.size) |
|
80201
6ac48d53d371
add HEAD to http server: should send same header fields as if request was GET;
Fabian Huch <huch@in.tum.de>
parents:
79717
diff
changeset
|
234 |
if (!is_head) using(http.getResponseBody)(output.write_stream) |
| 65078 | 235 |
} |
236 |
} |
|
237 |
||
238 |
||
| 75107 | 239 |
/* service */ |
| 66207 | 240 |
|
| 75393 | 241 |
abstract class Service(val name: String, method: String = "GET") {
|
| 75146 | 242 |
override def toString: String = name |
| 75113 | 243 |
|
244 |
def apply(request: Request): Option[Response] |
|
245 |
||
| 75146 | 246 |
def context(server_name: String): String = |
247 |
proper_string(url_path(server_name, name)).getOrElse("/")
|
|
| 75113 | 248 |
|
| 75394 | 249 |
def handler(server_name: String): HttpHandler = { (http: HttpExchange) =>
|
| 75113 | 250 |
val uri = http.getRequestURI |
251 |
val input = using(http.getRequestBody)(Bytes.read_stream(_)) |
|
|
80201
6ac48d53d371
add HEAD to http server: should send same header fields as if request was GET;
Fabian Huch <huch@in.tum.de>
parents:
79717
diff
changeset
|
252 |
val is_head = http.getRequestMethod == "HEAD" && method == "GET" |
|
6ac48d53d371
add HEAD to http server: should send same header fields as if request was GET;
Fabian Huch <huch@in.tum.de>
parents:
79717
diff
changeset
|
253 |
if (http.getRequestMethod == method || is_head) {
|
| 75146 | 254 |
val request = new Request(server_name, name, uri, input) |
|
78768
280a228dc2f1
prefer Exn.result: avoid accidental capture of interrupts, similar to ML;
wenzelm
parents:
78243
diff
changeset
|
255 |
Exn.result(apply(request)) match {
|
| 75113 | 256 |
case Exn.Res(Some(response)) => |
|
80201
6ac48d53d371
add HEAD to http server: should send same header fields as if request was GET;
Fabian Huch <huch@in.tum.de>
parents:
79717
diff
changeset
|
257 |
response.write(http, 200, is_head) |
| 75113 | 258 |
case Exn.Res(None) => |
|
80201
6ac48d53d371
add HEAD to http server: should send same header fields as if request was GET;
Fabian Huch <huch@in.tum.de>
parents:
79717
diff
changeset
|
259 |
Response.empty.write(http, 404, is_head) |
| 75113 | 260 |
case Exn.Exn(ERROR(msg)) => |
|
80201
6ac48d53d371
add HEAD to http server: should send same header fields as if request was GET;
Fabian Huch <huch@in.tum.de>
parents:
79717
diff
changeset
|
261 |
Response.text(Output.error_message_text(msg)).write(http, 500, is_head) |
| 75113 | 262 |
case Exn.Exn(exn) => throw exn |
| 75107 | 263 |
} |
| 75113 | 264 |
} |
265 |
else Response.empty.write(http, 400) |
|
| 75107 | 266 |
} |
| 73413 | 267 |
} |
| 66207 | 268 |
|
| 65077 | 269 |
|
| 81781 | 270 |
/* REST service (via JSON) */ |
271 |
||
272 |
abstract class REST_Service( |
|
273 |
name: String, |
|
274 |
progress: Progress = new Progress, |
|
275 |
method: String = "POST" |
|
276 |
) extends Service(name, method = method) {
|
|
277 |
def handle(body: JSON.T): Option[JSON.T] |
|
278 |
||
279 |
def apply(request: Request): Option[Response] = |
|
280 |
try {
|
|
281 |
for {
|
|
282 |
json <- |
|
283 |
Exn.capture(JSON.parse(request.input.text)) match {
|
|
284 |
case Exn.Res(json) => Some(json) |
|
285 |
case _ => |
|
286 |
progress.echo("Could not parse: " + quote(request.input.text), verbose = true)
|
|
287 |
None |
|
288 |
} |
|
289 |
res <- |
|
290 |
handle(json) match {
|
|
291 |
case Some(res) => Some(res) |
|
292 |
case None => |
|
293 |
progress.echo("Invalid request: " + JSON.Format(json), verbose = true)
|
|
294 |
None |
|
295 |
} |
|
296 |
} yield Response(Bytes(JSON.Format(res)), content_type = "application/json") |
|
297 |
} |
|
298 |
catch { case exn: Throwable =>
|
|
299 |
val uuid = UUID.random() |
|
300 |
progress.echo_error_message("Server error <" + uuid + ">: " + exn)
|
|
301 |
Some(Response.text("internal server error: " + uuid))
|
|
302 |
} |
|
303 |
} |
|
304 |
||
305 |
||
| 65077 | 306 |
/* server */ |
307 |
||
| 75393 | 308 |
class Server private[HTTP](val name: String, val http_server: HttpServer) {
|
| 75107 | 309 |
def += (service: Service): Unit = |
| 75108 | 310 |
http_server.createContext(service.context(name), service.handler(name)) |
| 75107 | 311 |
def -= (service: Service): Unit = |
| 75108 | 312 |
http_server.removeContext(service.context(name)) |
| 65077 | 313 |
|
| 73439 | 314 |
def start(): Unit = http_server.start() |
| 73367 | 315 |
def stop(): Unit = http_server.stop(0) |
| 65077 | 316 |
|
317 |
def address: InetSocketAddress = http_server.getAddress |
|
| 75107 | 318 |
|
| 75108 | 319 |
def url: String = "http://" + address.getHostName + ":" + address.getPort + url_path(name) |
| 65077 | 320 |
override def toString: String = url |
321 |
} |
|
322 |
||
| 75107 | 323 |
def server( |
| 76270 | 324 |
port: Int = 0, |
| 79717 | 325 |
name: String = UUID.random_string(), |
| 75393 | 326 |
services: List[Service] = isabelle_services |
327 |
): Server = {
|
|
| 76270 | 328 |
val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, port), 0) |
| 65077 | 329 |
http_server.setExecutor(null) |
| 65076 | 330 |
|
| 75107 | 331 |
val server = new Server(name, http_server) |
332 |
for (service <- services) server += service |
|
| 65077 | 333 |
server |
| 63823 | 334 |
} |
| 65079 | 335 |
|
336 |
||
| 65081 | 337 |
|
| 75107 | 338 |
/** Isabelle services **/ |
| 65081 | 339 |
|
| 75113 | 340 |
def isabelle_services: List[Service] = |
|
82107
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
341 |
List(Welcome_Service, Fonts_Service, CSS_Service, PDFjs_Service, Docs_Service) |
| 65081 | 342 |
|
343 |
||
344 |
/* welcome */ |
|
345 |
||
| 75145 | 346 |
object Welcome_Service extends Welcome() |
347 |
||
| 75393 | 348 |
class Welcome(name: String = "") extends Service(name) {
|
| 75113 | 349 |
def apply(request: Request): Option[Response] = |
350 |
if (request.toplevel) {
|
|
351 |
Some(Response.text("Welcome to " + Isabelle_System.identification()))
|
|
352 |
} |
|
353 |
else None |
|
354 |
} |
|
| 65081 | 355 |
|
356 |
||
357 |
/* fonts */ |
|
| 65079 | 358 |
|
| 75145 | 359 |
object Fonts_Service extends Fonts() |
360 |
||
| 75393 | 361 |
class Fonts(name: String = "fonts") extends Service(name) {
|
| 75113 | 362 |
private lazy val html_fonts: List[Isabelle_Fonts.Entry] = |
363 |
Isabelle_Fonts.fonts(hidden = true) |
|
| 65079 | 364 |
|
| 75113 | 365 |
def apply(request: Request): Option[Response] = |
366 |
if (request.toplevel) {
|
|
367 |
Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name)))) |
|
368 |
} |
|
369 |
else {
|
|
370 |
request.uri_path.flatMap(path => |
|
371 |
html_fonts.collectFirst( |
|
372 |
{ case entry if path == entry.path.base => Response(entry.bytes) }
|
|
373 |
)) |
|
374 |
} |
|
375 |
} |
|
|
75105
03115c9eea00
support for PDF.js: platform-independent PDF viewer;
wenzelm
parents:
75104
diff
changeset
|
376 |
|
|
03115c9eea00
support for PDF.js: platform-independent PDF viewer;
wenzelm
parents:
75104
diff
changeset
|
377 |
|
|
82107
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
378 |
/* css */ |
|
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
379 |
|
|
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
380 |
object CSS_Service extends CSS() |
|
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
381 |
|
|
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
382 |
class CSS(name: String = "css", fonts: String = Fonts_Service.name) extends Service(name) {
|
|
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
383 |
private lazy val css = |
|
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
384 |
HTML.fonts_css("/" + fonts + "/" + _) + "\n\n" + File.read(HTML.isabelle_css)
|
|
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
385 |
|
|
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
386 |
def apply(request: Request): Option[Response] = |
|
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
387 |
Some(Response(Bytes(css), Content.mime_type_css)) |
|
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
388 |
} |
|
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
389 |
|
|
6c3b7d1f2115
css service, e.g. for dynamic web apps;
Fabian Huch <huch@in.tum.de>
parents:
82106
diff
changeset
|
390 |
|
|
75105
03115c9eea00
support for PDF.js: platform-independent PDF viewer;
wenzelm
parents:
75104
diff
changeset
|
391 |
/* pdfjs */ |
|
03115c9eea00
support for PDF.js: platform-independent PDF viewer;
wenzelm
parents:
75104
diff
changeset
|
392 |
|
| 75145 | 393 |
object PDFjs_Service extends PDFjs() |
394 |
||
| 75393 | 395 |
class PDFjs(name: String = "pdfjs") extends Service(name) {
|
| 75113 | 396 |
def apply(request: Request): Option[Response] = |
|
75105
03115c9eea00
support for PDF.js: platform-independent PDF viewer;
wenzelm
parents:
75104
diff
changeset
|
397 |
for {
|
| 75107 | 398 |
p <- request.uri_path |
| 75117 | 399 |
path = Path.explode("$ISABELLE_PDFJS_HOME") + p if path.is_file
|
400 |
s = p.implode if s.startsWith("build/") || s.startsWith("web/")
|
|
| 75113 | 401 |
} yield Response.read(path) |
402 |
} |
|
| 75119 | 403 |
|
404 |
||
405 |
/* docs */ |
|
406 |
||
| 75145 | 407 |
object Docs_Service extends Docs() |
408 |
||
| 75393 | 409 |
class Docs(name: String = "docs") extends PDFjs(name) {
|
| 75119 | 410 |
private val doc_contents = isabelle.Doc.main_contents() |
411 |
||
| 75121 | 412 |
// example: .../docs/web/viewer.html?file=system.pdf |
| 75119 | 413 |
def doc_request(request: Request): Option[Response] = |
414 |
for {
|
|
415 |
p <- request.uri_path if p.is_pdf |
|
| 75121 | 416 |
s = p.implode if s.startsWith("web/")
|
| 75119 | 417 |
name = p.base.split_ext._1.implode |
|
81350
1818358373e2
misc tuning and clarification: Doc.Entry supports both plain files and pdf documents;
wenzelm
parents:
80368
diff
changeset
|
418 |
entry <- doc_contents.entries(name = _ == name, pdf = true).headOption |
|
1818358373e2
misc tuning and clarification: Doc.Entry supports both plain files and pdf documents;
wenzelm
parents:
80368
diff
changeset
|
419 |
} yield Response.read(entry.path) |
| 75119 | 420 |
|
421 |
override def apply(request: Request): Option[Response] = |
|
422 |
doc_request(request) orElse super.apply(request) |
|
423 |
} |
|
424 |
} |