# HG changeset patch
# User wenzelm
# Date 1617184972 -7200
# Node ID c42144d9dde6104001b2ea11b4eec0de60e50139
# Parent  d3f2038198aeffaa8b1465da569e1fe7d6180536
more uniform HTTP resources;

diff -r d3f2038198ae -r c42144d9dde6 src/Pure/General/http.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))
       }
diff -r d3f2038198ae -r c42144d9dde6 src/Tools/jEdit/src/document_model.scala
--- 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)
   }
 }