# HG changeset patch
# User wenzelm
# Date 1645796558 -3600
# Node ID 1ef43607aef246af8b068cfed83cf2a5a01e3a0c
# Parent  e721880779bed268db28130114b911c83c6fbd9d
clarified signature;

diff -r e721880779be -r 1ef43607aef2 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Fri Feb 25 14:38:16 2022 +0100
+++ b/src/Pure/General/http.scala	Fri Feb 25 14:42:38 2022 +0100
@@ -174,12 +174,12 @@
     names.iterator.flatMap(a => if (a.isEmpty) None else Some("/" + a)).mkString
 
   class Request private[HTTP](
-    val server: String,
-    val service: String,
+    val server_name: String,
+    val service_name: String,
     val uri: URI,
     val input: Bytes)
   {
-    def home: String = url_path(server, service)
+    def home: String = url_path(server_name, service_name)
     def root: String = home + "/"
     def query: String = home + "?"
 
@@ -239,19 +239,20 @@
 
   /* service */
 
-  abstract class Service(val service: String, method: String = "GET")
+  abstract class Service(val name: String, method: String = "GET")
   {
-    override def toString: String = service
+    override def toString: String = name
 
     def apply(request: Request): Option[Response]
 
-    def context(server: String): String = proper_string(url_path(server, service)).getOrElse("/")
+    def context(server_name: String): String =
+      proper_string(url_path(server_name, name)).getOrElse("/")
 
-    def handler(server: String): HttpHandler = (http: HttpExchange) => {
+    def handler(server_name: String): HttpHandler = (http: HttpExchange) => {
       val uri = http.getRequestURI
       val input = using(http.getRequestBody)(Bytes.read_stream(_))
       if (http.getRequestMethod == method) {
-        val request = new Request(server, service, uri, input)
+        val request = new Request(server_name, name, uri, input)
         Exn.capture(apply(request)) match {
           case Exn.Res(Some(response)) =>
             response.write(http, 200)
diff -r e721880779be -r 1ef43607aef2 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Feb 25 14:38:16 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Feb 25 14:42:38 2022 +0100
@@ -303,7 +303,7 @@
       case Some(model) =>
         val name = model.node_name
         val url =
-          PIDE.plugin.http_server.url + "/" + Preview_Service.service + "?" +
+          PIDE.plugin.http_server.url + "/" + Preview_Service.name + "?" +
               (if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
         PIDE.editor.hyperlink_url(url).follow(view)
       case _ =>
@@ -332,7 +332,7 @@
           Presentation.html_document(
             snapshot, html_context, Presentation.elements2,
             plain_text = query.startsWith(plain_text_prefix),
-            fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server)))
+            fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server_name)))
         HTTP.Response.html(document.content)
       }
   }