# HG changeset patch
# User wenzelm
# Date 1498598472 -7200
# Node ID 8d5cb4ea2b7cc76f46b8a180fb3b186a3534fbad
# Parent  2d2082db735adcc36907a2381ec4b5de67383b7a
support for HTTP/POST method;
more explict type HTTP.Arg;

diff -r 2d2082db735a -r 8d5cb4ea2b7c src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Tue Jun 27 21:56:56 2017 +0200
+++ b/src/Pure/General/http.scala	Tue Jun 27 23:21:12 2017 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.net.{InetAddress, InetSocketAddress, URI}
+import java.net.{InetAddress, InetSocketAddress, URI, URLDecoder}
 import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
 
 import scala.collection.immutable.SortedMap
@@ -66,12 +66,28 @@
   def handler(root: String, body: Exchange => Unit): Handler =
     new Handler(root, new HttpHandler { def handle(x: HttpExchange) { body(new Exchange(x)) } })
 
-  def get(root: String, body: URI => Option[Response]): Handler =
+
+  /* particular methods */
+
+  sealed case class Arg(method: String, uri: URI, request: Bytes)
+  {
+    def decode_properties: Properties.T =
+      Library.space_explode('&', request.text).map(s =>
+        Library.space_explode('=', s) match {
+          case List(a, b) =>
+            URLDecoder.decode(a, UTF8.charset_name) ->
+            URLDecoder.decode(b, UTF8.charset_name)
+          case _ => error("Malformed key-value pair in HTTP/POST: " + quote(s))
+        })
+  }
+
+  def method(name: String, root: String, body: Arg => Option[Response]): Handler =
     handler(root, http =>
       {
-        http.read_request()
-        if (http.request_method == "GET")
-          Exn.capture(body(http.request_uri)) match {
+        val request = http.read_request()
+        if (http.request_method == name) {
+          val arg = Arg(name, http.request_uri, request)
+          Exn.capture(body(arg)) match {
             case Exn.Res(Some(response)) =>
               http.write_response(200, response)
             case Exn.Res(None) =>
@@ -80,9 +96,13 @@
               http.write_response(500, Response.text(Output.error_message_text(msg)))
             case Exn.Exn(exn) => throw exn
           }
+        }
         else http.write_response(400, Response.empty)
       })
 
+  def get(root: String, body: Arg => Option[Response]): Handler = method("GET", root, body)
+  def post(root: String, body: Arg => Option[Response]): Handler = method("POST", root, body)
+
 
   /* server */
 
diff -r 2d2082db735a -r 8d5cb4ea2b7c src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Jun 27 21:56:56 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Jun 27 23:21:12 2017 +0200
@@ -301,9 +301,9 @@
   {
     val preview_root = http_root + "/preview"
     val preview =
-      HTTP.get(preview_root, uri =>
+      HTTP.get(preview_root, arg =>
         for {
-          theory <- Library.try_unprefix(preview_root + "/", uri.toString)
+          theory <- Library.try_unprefix(preview_root + "/", arg.uri.toString)
           model <-
             get_models().iterator.collectFirst(
               { case (node_name, model) if node_name.theory == theory => model })