--- /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
+ }
+}
--- 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
-}
--- 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