# HG changeset patch
# User wenzelm
# Date 1488454267 -3600
# Node ID 2d6e716c9d6eda1565bbb3e88bf281742621d4f1
# Parent  8a96ab58f016a0e9f1f263d4fe69c580c27d6b78
clarified modules;

diff -r 8a96ab58f016 -r 2d6e716c9d6e src/Pure/General/http.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/http.scala	Thu Mar 02 12:31:07 2017 +0100
@@ -0,0 +1,52 @@
+/*  Title:      Pure/General/http.scala
+    Author:     Makarius
+
+HTTP server support.
+*/
+
+package isabelle
+
+
+import java.net.{InetAddress, InetSocketAddress}
+import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
+
+
+object HTTP
+{
+  /* handler */
+
+  class Handler private[HTTP](val path: String, val handler: HttpHandler)
+  {
+    override def toString: String = path
+  }
+
+  def handler(path: String, body: HttpExchange => Unit): Handler =
+    new Handler(path, new HttpHandler { def handle(x: HttpExchange) { body(x) } })
+
+
+  /* server */
+
+  class Server private[HTTP](val http_server: HttpServer)
+  {
+    def += (handler: Handler) { http_server.createContext(handler.path, handler.handler) }
+    def -= (handler: Handler) { http_server.removeContext(handler.path) }
+
+    def start: Unit = http_server.start
+    def stop: Unit = http_server.stop(0)
+
+    def address: InetSocketAddress = http_server.getAddress
+    def url: String = "http://" + address.getHostName + ":" + address.getPort
+    override def toString: String = url
+  }
+
+  def server(handlers: Handler*): Server =
+  {
+    val localhost = InetAddress.getByName("127.0.0.1")
+    val http_server = HttpServer.create(new InetSocketAddress(localhost, 0), 0)
+    http_server.setExecutor(null)
+
+    val server = new Server(http_server)
+    for (handler <- handlers) server += handler
+    server
+  }
+}
diff -r 8a96ab58f016 -r 2d6e716c9d6e src/Pure/General/http_server.scala
--- a/src/Pure/General/http_server.scala	Thu Mar 02 12:09:50 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-/*  Title:      Pure/General/http_server.scala
-    Author:     Makarius
-
-Minimal HTTP server.
-*/
-
-package isabelle
-
-
-import java.net.{InetAddress, InetSocketAddress}
-import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
-
-
-object HTTP_Server
-{
-  class Handler private[HTTP_Server](val path: String, val handler: HttpHandler)
-  {
-    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 apply(handlers: Handler*): HTTP_Server =
-  {
-    val localhost = InetAddress.getByName("127.0.0.1")
-
-    val server = HttpServer.create(new InetSocketAddress(localhost, 0), 0)
-    server.setExecutor(null)
-
-    val http_server = new HTTP_Server(server)
-    for (handler <- handlers) http_server += handler
-    http_server
-  }
-}
-
-class HTTP_Server private(val server: HttpServer)
-{
-  def += (handler: HTTP_Server.Handler) { server.createContext(handler.path, handler.handler) }
-  def -= (handler: HTTP_Server.Handler) { server.removeContext(handler.path) }
-
-  def start: Unit = server.start
-  def stop: Unit = server.stop(0)
-
-  def address: InetSocketAddress = server.getAddress
-  def url: String = "http://" + address.getHostName + ":" + address.getPort
-  override def toString: String = url
-}
diff -r 8a96ab58f016 -r 2d6e716c9d6e src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Mar 02 12:09:50 2017 +0100
+++ b/src/Pure/build-jars	Thu Mar 02 12:31:07 2017 +0100
@@ -51,7 +51,7 @@
   General/graph.scala
   General/graph_display.scala
   General/graphics_file.scala
-  General/http_server.scala
+  General/http.scala
   General/json.scala
   General/linear_set.scala
   General/logger.scala