# HG changeset patch
# User wenzelm
# Date 1718567649 -7200
# Node ID 94875d8cc8bd2e9b58cf077b7c8cca331f612e0c
# Parent  2503ff5d29ce9e819895832bce463a8356f85c86# Parent  46135b44b1a37a940be67360efdf346cdceb4dbc
merged

diff -r 46135b44b1a3 -r 94875d8cc8bd src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Sun Jun 16 21:53:24 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Sun Jun 16 21:54:09 2024 +0200
@@ -916,6 +916,7 @@
         ci_job.trigger match {
           case isabelle.CI_Build.Timed(in_interval) if in_interval(previous, next) =>
             val task = Task(CI_Build(ci_job), ci_job.hosts.hosts_spec, isabelle_rev = "default")
+            echo("Triggered task " + task.kind)
             _state = _state.add_pending(task)
           case _ =>
         }
@@ -940,6 +941,9 @@
       val BUILD = Path.basic("build")
     }
 
+    def paths(store: Store): Web_App.Paths =
+      Web_App.Paths(store.address, Path.current, serve_frontend = true, landing = Page.HOME)
+
     object API {
       val BUILD_CANCEL = Path.explode("api/build/cancel")
     }
@@ -972,11 +976,12 @@
     }
   }
 
-  class Web_Server(port: Int, paths: Web_App.Paths, store: Store, progress: Progress)
+  class Web_Server(port: Int, store: Store, progress: Progress)
     extends Loop_Process[Unit]("Web_Server", store, progress) {
     import Web_App.*
     import Web_Server.*
 
+    val paths = Web_Server.paths(store)
     val cache = Cache.empty
 
     enum Model {
@@ -1279,6 +1284,7 @@
   case class Store(options: Options) {
     val base_dir = Path.explode(options.string("build_manager_dir"))
     val identifier = options.string("build_manager_identifier")
+    val address = Url(options.string("build_manager_address"))
 
     val pending = base_dir + Path.basic("pending")
     val finished = base_dir + Path.basic("finished")
@@ -1339,8 +1345,8 @@
     val isabelle_repository = Mercurial.self_repository()
     val ci_jobs =
       space_explode(',', options.string("build_manager_ci_jobs")).map(isabelle.CI_Build.the_job)
-    val url = Url(options.string("build_manager_address"))
-    val paths = Web_App.Paths(url, Path.current, true, Web_Server.Page.HOME)
+
+    progress.echo_if(ci_jobs.nonEmpty, "Managing ci jobs: " + commas_quote(ci_jobs.map(_.name)))
 
     using(store.open_database())(db =>
       Build_Manager.private_data.transaction_lock(db,
@@ -1350,7 +1356,7 @@
       new Runner(store, build_hosts, isabelle_repository, sync_dirs, progress),
       new Poller(ci_jobs, store, isabelle_repository, sync_dirs, progress),
       new Timer(ci_jobs, store, isabelle_repository, sync_dirs, progress),
-      new Web_Server(port, paths, store, progress))
+      new Web_Server(port, store, progress))
 
     val threads = processes.map(Isabelle_Thread.create(_))
     POSIX_Interrupt.handler {
@@ -1509,7 +1515,7 @@
     val afp_rev = if (afp_root.nonEmpty) Some("") else None
 
     val hosts_spec = options.string("build_manager_cluster")
-    val paths = Web_App.Paths(Url(options.string("build_manager_address")), Path.current)
+    val paths = Web_Server.paths(store)
 
     val build_config = User_Build(afp_rev, prefs, requirements, all_sessions,
       base_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions, build_heap,
diff -r 46135b44b1a3 -r 94875d8cc8bd src/Pure/System/web_app.scala
--- a/src/Pure/System/web_app.scala	Sun Jun 16 21:53:24 2024 +0200
+++ b/src/Pure/System/web_app.scala	Sun Jun 16 21:54:09 2024 +0200
@@ -297,12 +297,15 @@
 
       def get(key: Key): Option[String] = params.get(key)
       def apply(key: Key): String = get(key).getOrElse("")
-      def list(key: Key): List[Key] =
-        (for {
-          key1 <- params.keys.toList
-          key2 <- key1.get(key)
-          i <- key2.num
-        } yield key + i).distinct
+      def list(key: Key): List[Key] = {
+        val indexes =
+          for {
+            key1 <- params.keys.toList
+            key2 <- key1.get(key)
+            i <- key2.num
+          } yield i
+        indexes.distinct.sorted.map(key + _)
+      }
 
       def file(key: Key): Option[Bytes] = files.get(key)
     }