more uniform HTTP resources;
authorwenzelm
Wed, 31 Mar 2021 12:02:52 +0200
changeset 73518 c42144d9dde6
parent 73517 d3f2038198ae
child 73519 8f485a199874
more uniform HTTP resources;
src/Pure/General/http.scala
src/Tools/jEdit/src/document_model.scala
--- 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)
   }
 }