# HG changeset patch
# User wenzelm
# Date 1739459988 -3600
# Node ID 5d2ed7e56a49fdb342df71dfd39f9ced1196edc3
# Parent  2ecab61b59f3889c44d0a21f28e11c49ddf0f530
tuned signature: more operations;

diff -r 2ecab61b59f3 -r 5d2ed7e56a49 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Feb 13 14:26:50 2025 +0100
+++ b/src/Pure/General/http.scala	Thu Feb 13 16:19:48 2025 +0100
@@ -254,6 +254,9 @@
   abstract class Service(val name: String, method: String = "GET") {
     override def toString: String = name
 
+    def index_path(prefix: String = name, index: String = ""): String =
+      Url.index_path(prefix = prefix, index = index)
+
     def apply(request: Request): Option[Response]
 
     def context(server_name: String): String =
diff -r 2ecab61b59f3 -r 5d2ed7e56a49 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Thu Feb 13 14:26:50 2025 +0100
+++ b/src/Pure/General/url.scala	Thu Feb 13 16:19:48 2025 +0100
@@ -154,6 +154,9 @@
 
   def dir_path(prefix: String, direct: Boolean = false): String =
     if (direct) direct_path(prefix) else prefix
+
+  def index_path(prefix: String = "", index: String = ""): String =
+    append_path(prefix, if (index.isEmpty) "index.html" else index)
 }
 
 final class Url private(val uri: URI) {
diff -r 2ecab61b59f3 -r 5d2ed7e56a49 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Thu Feb 13 14:26:50 2025 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Thu Feb 13 16:19:48 2025 +0100
@@ -598,9 +598,7 @@
   /* HTTP browser_info */
 
   def open_browser_info(view: View): Unit = {
-    val url =
-      Url.append_path(PIDE.plugin.http_server.url,
-        Url.append_path(HTTP.Browser_Info_Service.name, "index.html"))
+    val url = Url.append_path(PIDE.plugin.http_server.url, HTTP.Browser_Info_Service.index_path())
     PIDE.editor.hyperlink_url(url).follow(view)
   }
 }