--- 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 =
--- 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) {
--- 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)
}
}