# 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 {