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 |
|
66207
|
10 |
import java.net.{InetAddress, InetSocketAddress, URI, URLDecoder}
|
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 =
|
|
48 |
using(http_exchange.getRequestBody)(Bytes.read_stream(_))
|
|
49 |
|
|
50 |
def write_response(code: Int, response: Response)
|
|
51 |
{
|
|
52 |
http_exchange.getResponseHeaders().set("Content-Type", response.content_type)
|
|
53 |
http_exchange.sendResponseHeaders(code, response.bytes.length.toLong)
|
|
54 |
using(http_exchange.getResponseBody)(response.bytes.write_stream(_))
|
|
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 =
|
|
67 |
new Handler(root, new HttpHandler { def handle(x: HttpExchange) { 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 =
|
|
75 |
Library.space_explode('&', request.text).map(s =>
|
|
76 |
Library.space_explode('=', s) match {
|
|
77 |
case List(a, b) =>
|
|
78 |
URLDecoder.decode(a, UTF8.charset_name) ->
|
|
79 |
URLDecoder.decode(b, UTF8.charset_name)
|
|
80 |
case _ => error("Malformed key-value pair in HTTP/POST: " + quote(s))
|
|
81 |
})
|
|
82 |
}
|
|
83 |
|
|
84 |
def method(name: String, root: String, body: Arg => Option[Response]): Handler =
|
65080
|
85 |
handler(root, http =>
|
65078
|
86 |
{
|
66207
|
87 |
val request = http.read_request()
|
|
88 |
if (http.request_method == name) {
|
|
89 |
val arg = Arg(name, http.request_uri, request)
|
|
90 |
Exn.capture(body(arg)) match {
|
65087
|
91 |
case Exn.Res(Some(response)) =>
|
|
92 |
http.write_response(200, response)
|
|
93 |
case Exn.Res(None) =>
|
|
94 |
http.write_response(404, Response.empty)
|
|
95 |
case Exn.Exn(ERROR(msg)) =>
|
65828
|
96 |
http.write_response(500, Response.text(Output.error_message_text(msg)))
|
65087
|
97 |
case Exn.Exn(exn) => throw exn
|
65078
|
98 |
}
|
66207
|
99 |
}
|
65078
|
100 |
else http.write_response(400, Response.empty)
|
|
101 |
})
|
65076
|
102 |
|
66207
|
103 |
def get(root: String, body: Arg => Option[Response]): Handler = method("GET", root, body)
|
|
104 |
def post(root: String, body: Arg => Option[Response]): Handler = method("POST", root, body)
|
|
105 |
|
65077
|
106 |
|
|
107 |
/* server */
|
|
108 |
|
|
109 |
class Server private[HTTP](val http_server: HttpServer)
|
|
110 |
{
|
65080
|
111 |
def += (handler: Handler) { http_server.createContext(handler.root, handler.handler) }
|
|
112 |
def -= (handler: Handler) { http_server.removeContext(handler.root) }
|
65077
|
113 |
|
|
114 |
def start: Unit = http_server.start
|
|
115 |
def stop: Unit = http_server.stop(0)
|
|
116 |
|
|
117 |
def address: InetSocketAddress = http_server.getAddress
|
|
118 |
def url: String = "http://" + address.getHostName + ":" + address.getPort
|
|
119 |
override def toString: String = url
|
|
120 |
}
|
|
121 |
|
65081
|
122 |
def server(handlers: List[Handler] = isabelle_resources): Server =
|
63823
|
123 |
{
|
|
124 |
val localhost = InetAddress.getByName("127.0.0.1")
|
65077
|
125 |
val http_server = HttpServer.create(new InetSocketAddress(localhost, 0), 0)
|
|
126 |
http_server.setExecutor(null)
|
65076
|
127 |
|
65077
|
128 |
val server = new Server(http_server)
|
|
129 |
for (handler <- handlers) server += handler
|
|
130 |
server
|
63823
|
131 |
}
|
65079
|
132 |
|
|
133 |
|
65081
|
134 |
|
|
135 |
/** Isabelle resources **/
|
|
136 |
|
|
137 |
lazy val isabelle_resources: List[Handler] =
|
65085
|
138 |
List(welcome, fonts())
|
65081
|
139 |
|
|
140 |
|
|
141 |
/* welcome */
|
|
142 |
|
65085
|
143 |
val welcome: Handler =
|
|
144 |
get("/", uri =>
|
65081
|
145 |
if (uri.toString == "/") {
|
|
146 |
val id =
|
|
147 |
Isabelle_System.getenv("ISABELLE_ID") match {
|
|
148 |
case "" => Mercurial.repository(Path.explode("~~")).id()
|
|
149 |
case id => id
|
|
150 |
}
|
65084
|
151 |
Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version))
|
65081
|
152 |
}
|
|
153 |
else None)
|
|
154 |
|
|
155 |
|
|
156 |
/* fonts */
|
65079
|
157 |
|
65086
|
158 |
private lazy val html_fonts: SortedMap[String, Bytes] =
|
65079
|
159 |
SortedMap(
|
65999
|
160 |
Isabelle_System.fonts(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
|
65079
|
161 |
|
|
162 |
def fonts(root: String = "/fonts"): Handler =
|
|
163 |
get(root, uri =>
|
|
164 |
{
|
|
165 |
val uri_name = uri.toString
|
65086
|
166 |
if (uri_name == root) Some(Response.text(cat_lines(html_fonts.map(_._1))))
|
|
167 |
else html_fonts.collectFirst({ case (a, b) if uri_name == root + "/" + a => Response(b) })
|
65079
|
168 |
})
|
63823
|
169 |
}
|