--- a/src/Pure/General/http.scala Wed Mar 31 11:24:46 2021 +0200
+++ b/src/Pure/General/http.scala Wed Mar 31 12:02:52 2021 +0200
@@ -271,14 +271,14 @@
/** Isabelle resources **/
lazy val isabelle_resources: List[Handler] =
- List(welcome, fonts())
+ List(welcome(), fonts())
/* welcome */
- val welcome: Handler =
- Handler.get("/", arg =>
- if (arg.uri.toString == "/") {
+ def welcome(root: String = "/"): Handler =
+ Handler.get(root, arg =>
+ if (arg.uri.toString == root) {
val id = Isabelle_System.isabelle_id()
Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version))
}
--- a/src/Tools/jEdit/src/document_model.scala Wed Mar 31 11:24:46 2021 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Mar 31 12:02:52 2021 +0200
@@ -330,7 +330,7 @@
HTTP.Response.html(document.content)
})
- List(HTTP.fonts(fonts_root), html)
+ List(HTTP.welcome(http_root), HTTP.fonts(fonts_root), html)
}
}