# HG changeset patch
# User wenzelm
# Date 1488460488 -3600
# Node ID 2b6ed26b7597e147c0fd9902e706b810be9756a1
# Parent  8a5c2b86c5f68691010f9d70bb860a8de570ef5c
tuned;

diff -r 8a5c2b86c5f6 -r 2b6ed26b7597 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Mar 02 14:10:41 2017 +0100
+++ b/src/Pure/General/http.scala	Thu Mar 02 14:14:48 2017 +0100
@@ -56,16 +56,16 @@
 
   /* handler */
 
-  class Handler private[HTTP](val path: String, val handler: HttpHandler)
+  class Handler private[HTTP](val root: String, val handler: HttpHandler)
   {
-    override def toString: String = path
+    override def toString: String = root
   }
 
-  def handler(path: String, body: Exchange => Unit): Handler =
-    new Handler(path, new HttpHandler { def handle(x: HttpExchange) { body(new Exchange(x)) } })
+  def handler(root: String, body: Exchange => Unit): Handler =
+    new Handler(root, new HttpHandler { def handle(x: HttpExchange) { body(new Exchange(x)) } })
 
-  def get(path: String, body: URI => Option[Response]): Handler =
-    handler(path, http =>
+  def get(root: String, body: URI => Option[Response]): Handler =
+    handler(root, http =>
       {
         http.read_request()
         if (http.request_method == "GET")
@@ -81,8 +81,8 @@
 
   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 += (handler: Handler) { http_server.createContext(handler.root, handler.handler) }
+    def -= (handler: Handler) { http_server.removeContext(handler.root) }
 
     def start: Unit = http_server.start
     def stop: Unit = http_server.stop(0)