equal
deleted
inserted
replaced
1 /* Title: Pure/General/http_server.scala |
|
2 Author: Makarius |
|
3 |
|
4 Minimal HTTP server. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 import java.net.{InetAddress, InetSocketAddress} |
|
11 import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer} |
|
12 |
|
13 |
|
14 object HTTP_Server |
|
15 { |
|
16 class Handler private[HTTP_Server](val path: String, val handler: HttpHandler) |
|
17 { |
|
18 override def toString: String = path |
|
19 } |
|
20 |
|
21 def handler(path: String)(body: HttpExchange => Unit): Handler = |
|
22 new Handler(path, new HttpHandler { def handle(x: HttpExchange) { body(x) } }) |
|
23 |
|
24 def apply(handlers: Handler*): HTTP_Server = |
|
25 { |
|
26 val localhost = InetAddress.getByName("127.0.0.1") |
|
27 |
|
28 val server = HttpServer.create(new InetSocketAddress(localhost, 0), 0) |
|
29 server.setExecutor(null) |
|
30 |
|
31 val http_server = new HTTP_Server(server) |
|
32 for (handler <- handlers) http_server += handler |
|
33 http_server |
|
34 } |
|
35 } |
|
36 |
|
37 class HTTP_Server private(val server: HttpServer) |
|
38 { |
|
39 def += (handler: HTTP_Server.Handler) { server.createContext(handler.path, handler.handler) } |
|
40 def -= (handler: HTTP_Server.Handler) { server.removeContext(handler.path) } |
|
41 |
|
42 def start: Unit = server.start |
|
43 def stop: Unit = server.stop(0) |
|
44 |
|
45 def address: InetSocketAddress = server.getAddress |
|
46 def url: String = "http://" + address.getHostName + ":" + address.getPort |
|
47 override def toString: String = url |
|
48 } |
|