--- a/src/Pure/General/http.scala Mon Feb 21 12:56:35 2022 +0100
+++ b/src/Pure/General/http.scala Mon Feb 21 13:15:35 2022 +0100
@@ -183,7 +183,9 @@
def root: String = home + "/"
def query: String = home + "?"
- def uri_name: String = uri.toString
+ def toplevel: Boolean = uri_name == home || uri_name == root
+
+ val uri_name: String = uri.toString
def uri_path: Option[Path] =
for {
@@ -315,10 +317,12 @@
def welcome(name: String = "welcome"): Service =
Service.get(name, request =>
- if (request.uri_name == request.home) {
- Some(Response.text("Welcome to " + Isabelle_System.identification()))
- }
- else None)
+ {
+ if (request.toplevel) {
+ Some(Response.text("Welcome to " + Isabelle_System.identification()))
+ }
+ else None
+ })
/* fonts */
@@ -329,7 +333,7 @@
def fonts(name: String = "fonts"): Service =
Service.get(name, request =>
{
- if (request.uri_name == request.home) {
+ if (request.toplevel) {
Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name))))
}
else {