src/Pure/General/http_server.scala
author traytel
Mon, 24 Oct 2016 16:53:32 +0200
changeset 64379 71f42dcaa1df
parent 63823 ca8b737b08cf
child 65076 8a96ab58f016
permissions -rw-r--r--
additional user-specified simp (naturality) rules used in friend_of_corec
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63823
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/http_server.scala
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     3
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     4
Minimal HTTP server.
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     5
*/
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     6
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     7
package isabelle
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     8
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     9
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    10
import java.net.{InetAddress, InetSocketAddress}
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    11
import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    12
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    13
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    14
object HTTP_Server
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    15
{
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    16
  def apply(handler: HttpExchange => Unit): HTTP_Server =
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    17
  {
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    18
    val localhost = InetAddress.getByName("127.0.0.1")
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    19
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    20
    val server = HttpServer.create(new InetSocketAddress(localhost, 0), 0)
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    21
    server.createContext("/", new HttpHandler { def handle(x: HttpExchange) { handler(x) } })
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    22
    server.setExecutor(null)
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    23
    new HTTP_Server(server)
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    24
  }
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    25
}
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    26
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    27
class HTTP_Server private(val server: HttpServer)
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    28
{
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    29
  def start: Unit = server.start
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    30
  def stop: Unit = server.stop(0)
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    31
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    32
  def address: InetSocketAddress = server.getAddress
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    33
  def url: String = "http://" + address.getHostName + ":" + address.getPort
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    34
  override def toString: String = url
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    35
}