clarified modules;
authorwenzelm
Thu Mar 02 12:31:07 2017 +0100 (2017-03-02)
changeset 650772d6e716c9d6e
parent 65076 8a96ab58f016
child 65078 2339994e8790
clarified modules;
src/Pure/General/http.scala
src/Pure/General/http_server.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/http.scala	Thu Mar 02 12:31:07 2017 +0100
     1.3 @@ -0,0 +1,52 @@
     1.4 +/*  Title:      Pure/General/http.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +HTTP server support.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.net.{InetAddress, InetSocketAddress}
    1.14 +import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
    1.15 +
    1.16 +
    1.17 +object HTTP
    1.18 +{
    1.19 +  /* handler */
    1.20 +
    1.21 +  class Handler private[HTTP](val path: String, val handler: HttpHandler)
    1.22 +  {
    1.23 +    override def toString: String = path
    1.24 +  }
    1.25 +
    1.26 +  def handler(path: String, body: HttpExchange => Unit): Handler =
    1.27 +    new Handler(path, new HttpHandler { def handle(x: HttpExchange) { body(x) } })
    1.28 +
    1.29 +
    1.30 +  /* server */
    1.31 +
    1.32 +  class Server private[HTTP](val http_server: HttpServer)
    1.33 +  {
    1.34 +    def += (handler: Handler) { http_server.createContext(handler.path, handler.handler) }
    1.35 +    def -= (handler: Handler) { http_server.removeContext(handler.path) }
    1.36 +
    1.37 +    def start: Unit = http_server.start
    1.38 +    def stop: Unit = http_server.stop(0)
    1.39 +
    1.40 +    def address: InetSocketAddress = http_server.getAddress
    1.41 +    def url: String = "http://" + address.getHostName + ":" + address.getPort
    1.42 +    override def toString: String = url
    1.43 +  }
    1.44 +
    1.45 +  def server(handlers: Handler*): Server =
    1.46 +  {
    1.47 +    val localhost = InetAddress.getByName("127.0.0.1")
    1.48 +    val http_server = HttpServer.create(new InetSocketAddress(localhost, 0), 0)
    1.49 +    http_server.setExecutor(null)
    1.50 +
    1.51 +    val server = new Server(http_server)
    1.52 +    for (handler <- handlers) server += handler
    1.53 +    server
    1.54 +  }
    1.55 +}
     2.1 --- a/src/Pure/General/http_server.scala	Thu Mar 02 12:09:50 2017 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,48 +0,0 @@
     2.4 -/*  Title:      Pure/General/http_server.scala
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Minimal HTTP server.
     2.8 -*/
     2.9 -
    2.10 -package isabelle
    2.11 -
    2.12 -
    2.13 -import java.net.{InetAddress, InetSocketAddress}
    2.14 -import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
    2.15 -
    2.16 -
    2.17 -object HTTP_Server
    2.18 -{
    2.19 -  class Handler private[HTTP_Server](val path: String, val handler: HttpHandler)
    2.20 -  {
    2.21 -    override def toString: String = path
    2.22 -  }
    2.23 -
    2.24 -  def handler(path: String)(body: HttpExchange => Unit): Handler =
    2.25 -    new Handler(path, new HttpHandler { def handle(x: HttpExchange) { body(x) } })
    2.26 -
    2.27 -  def apply(handlers: Handler*): HTTP_Server =
    2.28 -  {
    2.29 -    val localhost = InetAddress.getByName("127.0.0.1")
    2.30 -
    2.31 -    val server = HttpServer.create(new InetSocketAddress(localhost, 0), 0)
    2.32 -    server.setExecutor(null)
    2.33 -
    2.34 -    val http_server = new HTTP_Server(server)
    2.35 -    for (handler <- handlers) http_server += handler
    2.36 -    http_server
    2.37 -  }
    2.38 -}
    2.39 -
    2.40 -class HTTP_Server private(val server: HttpServer)
    2.41 -{
    2.42 -  def += (handler: HTTP_Server.Handler) { server.createContext(handler.path, handler.handler) }
    2.43 -  def -= (handler: HTTP_Server.Handler) { server.removeContext(handler.path) }
    2.44 -
    2.45 -  def start: Unit = server.start
    2.46 -  def stop: Unit = server.stop(0)
    2.47 -
    2.48 -  def address: InetSocketAddress = server.getAddress
    2.49 -  def url: String = "http://" + address.getHostName + ":" + address.getPort
    2.50 -  override def toString: String = url
    2.51 -}
     3.1 --- a/src/Pure/build-jars	Thu Mar 02 12:09:50 2017 +0100
     3.2 +++ b/src/Pure/build-jars	Thu Mar 02 12:31:07 2017 +0100
     3.3 @@ -51,7 +51,7 @@
     3.4    General/graph.scala
     3.5    General/graph_display.scala
     3.6    General/graphics_file.scala
     3.7 -  General/http_server.scala
     3.8 +  General/http.scala
     3.9    General/json.scala
    3.10    General/linear_set.scala
    3.11    General/logger.scala