clarified signature;

--- a/src/Pure/General/http.scala	Sun Feb 20 22:14:30 2022 +0100
+++ b/src/Pure/General/http.scala	Mon Feb 21 12:56:35 2022 +0100
@@ -170,8 +170,16 @@
 
   /* request */
 
-  class Request private[HTTP](val home: String, val uri: URI, val input: Bytes)
+  def url_path(names: String*): String =
+    names.iterator.flatMap(a => if (a.isEmpty) None else Some("/" + a)).mkString
+
+  class Request private[HTTP](
+    val server: String,
+    val service: String,
+    val uri: URI,
+    val input: Bytes)
   {
+    def home: String = url_path(server, service)
     def root: String = home + "/"
     def query: String = home + "?"
 
@@ -239,7 +247,7 @@
           val uri = http.getRequestURI
           val input = using(http.getRequestBody)(Bytes.read_stream(_))
           if (http.getRequestMethod == method) {
-            val request = new Request(home(server), uri, input)
+            val request = new Request(server, name, uri, input)
             Exn.capture(body(request)) match {
               case Exn.Res(Some(response)) =>
                 response.write(http, 200)
@@ -261,8 +269,7 @@
   abstract class Service private[HTTP](val name: String)
   {
     override def toString: String = name
-    def home(server: String): String =
-      (if (server.isEmpty) "" else "" + "/" + server) + "/" + name
+    def context(server: String): String = proper_string(url_path(server, name)).getOrElse("/")
     def handler(server: String): HttpHandler
   }
 
@@ -272,19 +279,16 @@
   class Server private[HTTP](val name: String, val http_server: HttpServer)
   {
     def += (service: Service): Unit =
-      http_server.createContext(service.home(name), service.handler(name))
+      http_server.createContext(service.context(name), service.handler(name))
     def -= (service: Service): Unit =
-      http_server.removeContext(service.home(name))
+      http_server.removeContext(service.context(name))
 
     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 +
-        (if (name.isEmpty) "" else "/" + name)
-
+    def url: String = "http://" + address.getHostName + ":" + address.getPort + url_path(name)
     override def toString: String = url
   }
 

--- a/src/Tools/jEdit/src/document_model.scala	Sun Feb 20 22:14:30 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Feb 21 12:56:35 2022 +0100
@@ -330,7 +330,7 @@
           Presentation.html_document(
             snapshot, html_context, Presentation.elements2,
             plain_text = query.startsWith(plain_text_prefix),
-            fonts_css = HTML.fonts_css_dir(Library.perhaps_unsuffix("/preview", request.home)))
+            fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server)))
         HTTP.Response.html(document.content)
       })
 }