# HG changeset patch
# User wenzelm
# Date 1473288201 -7200
# Node ID ca8b737b08cf7645c73dc8ef466d5c66010853a8
# Parent  c575a3814a76cb1bdd262840c8fee8311377f3b4
minimal HTTP server;

diff -r c575a3814a76 -r ca8b737b08cf src/Pure/General/http_server.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/http_server.scala	Thu Sep 08 00:43:21 2016 +0200
@@ -0,0 +1,35 @@
+/*  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
+{
+  def apply(handler: HttpExchange => Unit): HTTP_Server =
+  {
+    val localhost = InetAddress.getByName("127.0.0.1")
+
+    val server = HttpServer.create(new InetSocketAddress(localhost, 0), 0)
+    server.createContext("/", new HttpHandler { def handle(x: HttpExchange) { handler(x) } })
+    server.setExecutor(null)
+    new HTTP_Server(server)
+  }
+}
+
+class HTTP_Server private(val server: HttpServer)
+{
+  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 c575a3814a76 -r ca8b737b08cf src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Sep 07 22:28:40 2016 +0200
+++ b/src/Pure/build-jars	Thu Sep 08 00:43:21 2016 +0200
@@ -32,6 +32,7 @@
   General/graph.scala
   General/graph_display.scala
   General/graphics_file.scala
+  General/http_server.scala
   General/json.scala
   General/linear_set.scala
   General/long_name.scala