# HG changeset patch
# User wenzelm
# Date 1488458167 -3600
# Node ID 2339994e879096a27396e31a01af5970160f230c
# Parent  2d6e716c9d6eda1565bbb3e88bf281742621d4f1
more operations;

diff -r 2d6e716c9d6e -r 2339994e8790 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Mar 02 12:31:07 2017 +0100
+++ b/src/Pure/General/http.scala	Thu Mar 02 13:36:07 2017 +0100
@@ -7,12 +7,51 @@
 package isabelle
 
 
-import java.net.{InetAddress, InetSocketAddress}
+import java.net.{InetAddress, InetSocketAddress, URI}
 import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
 
 
 object HTTP
 {
+  /* response */
+
+  object Response
+  {
+    def apply(
+        bytes: Bytes = Bytes.empty,
+        content_type: String = "application/octet-stream"): Response =
+      new Response(bytes, content_type)
+
+    val empty: Response = apply()
+    def text(s: String): Response = apply(Bytes(s), "text/plain; charset=utf-8")
+    def html(s: String): Response = apply(Bytes(s), "text/html; charset=utf-8")
+  }
+
+  class Response private[HTTP](val bytes: Bytes, val content_type: String)
+  {
+    override def toString: String = bytes.toString
+  }
+
+
+  /* exchange */
+
+  class Exchange private[HTTP](val http_exchange: HttpExchange)
+  {
+    def request_method: String = http_exchange.getRequestMethod
+    def request_uri: URI = http_exchange.getRequestURI
+
+    def read_request(): Bytes =
+      using(http_exchange.getRequestBody)(Bytes.read_stream(_))
+
+    def write_response(code: Int, response: Response)
+    {
+      http_exchange.getResponseHeaders().set("Content-Type", response.content_type)
+      http_exchange.sendResponseHeaders(code, response.bytes.length.toLong)
+      using(http_exchange.getResponseBody)(response.bytes.write_stream(_))
+    }
+  }
+
+
   /* handler */
 
   class Handler private[HTTP](val path: String, val handler: HttpHandler)
@@ -20,8 +59,20 @@
     override def toString: String = path
   }
 
-  def handler(path: String, body: HttpExchange => Unit): Handler =
-    new Handler(path, new HttpHandler { def handle(x: HttpExchange) { body(x) } })
+  def handler(path: String, body: Exchange => Unit): Handler =
+    new Handler(path, new HttpHandler { def handle(x: HttpExchange) { body(new Exchange(x)) } })
+
+  def get(path: String, body: URI => Option[Response]): Handler =
+    handler(path, http =>
+      {
+        http.read_request()
+        if (http.request_method == "GET")
+          body(http.request_uri) match {
+            case None => http.write_response(404, Response.empty)
+            case Some(response) => http.write_response(200, response)
+          }
+        else http.write_response(400, Response.empty)
+      })
 
 
   /* server */