author | wenzelm |
Mon, 01 Mar 2021 22:22:12 +0100 | |
changeset 73340 | 0ffcad1f6130 |
parent 69463 | 6439c9024dcc |
child 73367 | 77ef8bef0593 |
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 = |
|
69393
ed0824ef337e
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents:
69374
diff
changeset
|
48 |
using(http_exchange.getRequestBody)(Bytes.read_stream(_)) |
65078 | 49 |
|
73340 | 50 |
def write_response(code: Int, response: Response): Unit = |
65078 | 51 |
{ |
52 |
http_exchange.getResponseHeaders().set("Content-Type", response.content_type) |
|
53 |
http_exchange.sendResponseHeaders(code, response.bytes.length.toLong) |
|
69393
ed0824ef337e
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents:
69374
diff
changeset
|
54 |
using(http_exchange.getResponseBody)(response.bytes.write_stream(_)) |
65078 | 55 |
} |
56 |
} |
|
57 |
||
58 |
||
65077 | 59 |
/* handler */ |
60 |
||
65080 | 61 |
class Handler private[HTTP](val root: String, val handler: HttpHandler) |
65076 | 62 |
{ |
65080 | 63 |
override def toString: String = root |
65076 | 64 |
} |
65 |
||
65080 | 66 |
def handler(root: String, body: Exchange => Unit): Handler = |
73340 | 67 |
new Handler(root, new HttpHandler { def handle(x: HttpExchange): Unit = body(new Exchange(x)) }) |
65078 | 68 |
|
66207 | 69 |
|
70 |
/* particular methods */ |
|
71 |
||
72 |
sealed case class Arg(method: String, uri: URI, request: Bytes) |
|
73 |
{ |
|
74 |
def decode_properties: Properties.T = |
|
66923 | 75 |
space_explode('&', request.text).map(s => |
76 |
space_explode('=', s) match { |
|
67245 | 77 |
case List(a, b) => Url.decode(a) -> Url.decode(b) |
66207 | 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 = |
|
65080 | 83 |
handler(root, http => |
65078 | 84 |
{ |
66207 | 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 { |
|
65087 | 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)) => |
|
65828 | 94 |
http.write_response(500, Response.text(Output.error_message_text(msg))) |
65087 | 95 |
case Exn.Exn(exn) => throw exn |
65078 | 96 |
} |
66207 | 97 |
} |
65078 | 98 |
else http.write_response(400, Response.empty) |
99 |
}) |
|
65076 | 100 |
|
66207 | 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 |
||
65077 | 104 |
|
105 |
/* server */ |
|
106 |
||
107 |
class Server private[HTTP](val http_server: HttpServer) |
|
108 |
{ |
|
73340 | 109 |
def += (handler: Handler): Unit = http_server.createContext(handler.root, handler.handler) |
110 |
def -= (handler: Handler): Unit = http_server.removeContext(handler.root) |
|
65077 | 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 |
||
65081 | 120 |
def server(handlers: List[Handler] = isabelle_resources): Server = |
63823 | 121 |
{ |
69463 | 122 |
val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0) |
65077 | 123 |
http_server.setExecutor(null) |
65076 | 124 |
|
65077 | 125 |
val server = new Server(http_server) |
126 |
for (handler <- handlers) server += handler |
|
127 |
server |
|
63823 | 128 |
} |
65079 | 129 |
|
130 |
||
65081 | 131 |
|
132 |
/** Isabelle resources **/ |
|
133 |
||
134 |
lazy val isabelle_resources: List[Handler] = |
|
65085 | 135 |
List(welcome, fonts()) |
65081 | 136 |
|
137 |
||
138 |
/* welcome */ |
|
139 |
||
65085 | 140 |
val welcome: Handler = |
66479 | 141 |
get("/", arg => |
142 |
if (arg.uri.toString == "/") { |
|
67865 | 143 |
val id = Isabelle_System.isabelle_id() |
65084 | 144 |
Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version)) |
65081 | 145 |
} |
146 |
else None) |
|
147 |
||
148 |
||
149 |
/* fonts */ |
|
65079 | 150 |
|
69374 | 151 |
private lazy val html_fonts: List[Isabelle_Fonts.Entry] = |
152 |
Isabelle_Fonts.fonts(hidden = true) |
|
65079 | 153 |
|
154 |
def fonts(root: String = "/fonts"): Handler = |
|
66479 | 155 |
get(root, arg => |
65079 | 156 |
{ |
66479 | 157 |
val uri_name = arg.uri.toString |
69364
91dbade9a5fa
proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents:
69363
diff
changeset
|
158 |
if (uri_name == root) { |
69366 | 159 |
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
|
160 |
} |
91dbade9a5fa
proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents:
69363
diff
changeset
|
161 |
else { |
91dbade9a5fa
proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents:
69363
diff
changeset
|
162 |
html_fonts.collectFirst( |
69366 | 163 |
{ 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
|
164 |
} |
65079 | 165 |
}) |
63823 | 166 |
} |