# HG changeset patch
# User wenzelm
# Date 1645445735 -3600
# Node ID e6162afc5460771e70d840f8753c0f0b2a088457
# Parent  05ba781cf890c6f321223d21375427ebcd748a9b
more robust toplevel url: allow extra "/";

diff -r 05ba781cf890 -r e6162afc5460 src/Pure/General/http.scala
--- 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 {