more robust toplevel url: allow extra "/";
authorwenzelm
Mon, 21 Feb 2022 13:15:35 +0100
changeset 75109 e6162afc5460
parent 75108 05ba781cf890
child 75110 3c8f24e9eff1
more robust toplevel url: allow extra "/";
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 {