1/*  Title:      Pure/General/http.scala
2    Author:     Makarius
3
4HTTP server support.
5*/
6
7package isabelle
8
9
10import java.net.{InetAddress, InetSocketAddress, URI}
11import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
12
13import scala.collection.immutable.SortedMap
14
15
16object HTTP
17{
18  /** server **/
19
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
59  /* handler */
60
61  class Handler private[HTTP](val root: String, val handler: HttpHandler)
62  {
63    override def toString: String = root
64  }
65
66  def handler(root: String, body: Exchange => Unit): Handler =
67    new Handler(root, new HttpHandler { def handle(x: HttpExchange) { body(new Exchange(x)) } })
68
69
70  /* particular methods */
71
72  sealed case class Arg(method: String, uri: URI, request: Bytes)
73  {
74    def decode_properties: Properties.T =
75      space_explode('&', request.text).map(s =>
76        space_explode('=', s) match {
77          case List(a, b) => Url.decode(a) -> Url.decode(b)
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 =
83    handler(root, http =>
84      {
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 {
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)) =>
94              http.write_response(500, Response.text(Output.error_message_text(msg)))
95            case Exn.Exn(exn) => throw exn
96          }
97        }
98        else http.write_response(400, Response.empty)
99      })
100
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
104
105  /* server */
106
107  class Server private[HTTP](val http_server: HttpServer)
108  {
109    def += (handler: Handler) { http_server.createContext(handler.root, handler.handler) }
110    def -= (handler: Handler) { http_server.removeContext(handler.root) }
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
120  def server(handlers: List[Handler] = isabelle_resources): Server =
121  {
122    val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0)
123    http_server.setExecutor(null)
124
125    val server = new Server(http_server)
126    for (handler <- handlers) server += handler
127    server
128  }
129
130
131
132  /** Isabelle resources **/
133
134  lazy val isabelle_resources: List[Handler] =
135    List(welcome, fonts())
136
137
138  /* welcome */
139
140  val welcome: Handler =
141    get("/", arg =>
142      if (arg.uri.toString == "/") {
143        val id = Isabelle_System.isabelle_id()
144        Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version))
145      }
146      else None)
147
148
149  /* fonts */
150
151  private lazy val html_fonts: List[Isabelle_Fonts.Entry] =
152    Isabelle_Fonts.fonts(hidden = true)
153
154  def fonts(root: String = "/fonts"): Handler =
155    get(root, arg =>
156      {
157        val uri_name = arg.uri.toString
158        if (uri_name == root) {
159          Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name))))
160        }
161        else {
162          html_fonts.collectFirst(
163            { case entry if uri_name == root + "/" + entry.path.file_name => Response(entry.bytes) })
164        }
165      })
166}
167