# HG changeset patch
# User wenzelm
# Date 1615491056 -3600
# Node ID 56c0a793cd8b8e7bda779ae3a57840f2b9070ac4
# Parent  83569d2436714e4e9a82e40bf679c46d6cb9a83b
clarified signature;

diff -r 83569d243671 -r 56c0a793cd8b src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Mar 11 12:16:17 2021 +0100
+++ b/src/Pure/General/http.scala	Thu Mar 11 20:30:56 2021 +0100
@@ -56,18 +56,7 @@
   }
 
 
-  /* handler */
-
-  class Handler private[HTTP](val root: String, val handler: HttpHandler)
-  {
-    override def toString: String = root
-  }
-
-  def handler(root: String, body: Exchange => Unit): Handler =
-    new Handler(root, new HttpHandler { def handle(x: HttpExchange): Unit = body(new Exchange(x)) })
-
-
-  /* particular methods */
+  /* handler for request method */
 
   sealed case class Arg(method: String, uri: URI, request: Bytes)
   {
@@ -79,27 +68,39 @@
         })
   }
 
-  def method(name: String, root: String, body: Arg => Option[Response]): Handler =
-    handler(root, http =>
-      {
-        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) =>
-              http.write_response(404, Response.empty)
-            case Exn.Exn(ERROR(msg)) =>
-              http.write_response(500, Response.text(Output.error_message_text(msg)))
-            case Exn.Exn(exn) => throw exn
+  object Handler
+  {
+    def apply(root: String, body: Exchange => Unit): Handler =
+      new Handler(root,
+        new HttpHandler { def handle(x: HttpExchange): Unit = body(new Exchange(x)) })
+
+    def method(name: String, root: String, body: Arg => Option[Response]): Handler =
+      apply(root, http =>
+        {
+          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) =>
+                http.write_response(404, Response.empty)
+              case Exn.Exn(ERROR(msg)) =>
+                http.write_response(500, Response.text(Output.error_message_text(msg)))
+              case Exn.Exn(exn) => throw exn
+            }
           }
-        }
-        else http.write_response(400, Response.empty)
-      })
+          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)
+    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)
+  }
+
+  class Handler private(val root: String, val handler: HttpHandler)
+  {
+    override def toString: String = root
+  }
 
 
   /* server */
@@ -138,7 +139,7 @@
   /* welcome */
 
   val welcome: Handler =
-    get("/", arg =>
+    Handler.get("/", arg =>
       if (arg.uri.toString == "/") {
         val id = Isabelle_System.isabelle_id()
         Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version))
@@ -152,7 +153,7 @@
     Isabelle_Fonts.fonts(hidden = true)
 
   def fonts(root: String = "/fonts"): Handler =
-    get(root, arg =>
+    Handler.get(root, arg =>
       {
         val uri_name = arg.uri.toString
         if (uri_name == root) {
diff -r 83569d243671 -r 56c0a793cd8b src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Mar 11 12:16:17 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Mar 11 20:30:56 2021 +0100
@@ -314,7 +314,7 @@
     val preview_root = http_root + "/preview"
 
     val html =
-      HTTP.get(preview_root, arg =>
+      HTTP.Handler.get(preview_root, arg =>
         for {
           query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode)
           name = Library.perhaps_unprefix(plain_text_prefix, query)