clarified web server paths;
authorFabian Huch <huch@in.tum.de>
Wed, 12 Jun 2024 08:52:36 +0200
changeset 80348 3b4f9e8b46cb
parent 80347 613ac8c77a84
child 80349 2503ff5d29ce
clarified web server paths;
src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Jun 11 14:27:04 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Wed Jun 12 08:52:36 2024 +0200
@@ -940,6 +940,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 +975,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 +1283,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 +1344,6 @@
     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)
 
     using(store.open_database())(db =>
       Build_Manager.private_data.transaction_lock(db,
@@ -1350,7 +1353,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 +1512,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,