src/Pure/Build/build_manager.scala
changeset 80412 a7f8249533e9
parent 80411 a9fce67fb8b2
child 80414 4b10ae56ed01
--- a/src/Pure/Build/build_manager.scala	Wed Jun 12 17:06:34 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Wed Jun 12 17:12:13 2024 +0200
@@ -39,7 +39,7 @@
   }
 
   object CI_Build {
-    def apply(job: isabelle.CI_Build.Job): CI_Build =
+    def apply(job: Build_CI.Job): CI_Build =
       CI_Build(job.name, job.hosts.build_cluster, job.components.map(Component(_, "default")))
   }
 
@@ -47,7 +47,7 @@
     extends Build_Config {
     def fresh_build: Boolean = true
     def command(job_url: Url, build_hosts: List[Build_Cluster.Host]): String =
-      " ci_build" +
+      " build_ci" +
       " -u " + Bash.string(job_url.toString) +
       if_proper(build_cluster, build_hosts.map(host => " -H " + Bash.string(host.print)).mkString) +
       " " + name
@@ -851,7 +851,7 @@
   }
 
   class Poller(
-    ci_jobs: List[isabelle.CI_Build.Job],
+    ci_jobs: List[Build_CI.Job],
     store: Store,
     isabelle_repository: Mercurial.Repository,
     sync_dirs: List[Sync.Dir],
@@ -881,7 +881,7 @@
       synchronized_database("add_tasks") {
         for {
           ci_job <- ci_jobs
-          if ci_job.trigger == isabelle.CI_Build.On_Commit
+          if ci_job.trigger == Build_CI.On_Commit
           if isabelle_updated || ci_job.components.exists(updated_components.contains)
           if !_state.pending.values.exists(_.kind == ci_job.name)
         } {
@@ -910,7 +910,7 @@
   }
 
   class Timer(
-    ci_jobs: List[isabelle.CI_Build.Job],
+    ci_jobs: List[Build_CI.Job],
     store: Store,
     isabelle_repository: Mercurial.Repository,
     sync_dirs: List[Sync.Dir],
@@ -922,7 +922,7 @@
     private def add_tasks(previous: Date, next: Date): Unit = synchronized_database("add_tasks") {
       for (ci_job <- ci_jobs)
         ci_job.trigger match {
-          case isabelle.CI_Build.Timed(in_interval) if in_interval(previous, next) =>
+          case Build_CI.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)
@@ -1354,8 +1354,7 @@
   ): Unit = {
     val store = Store(options)
     val isabelle_repository = Mercurial.self_repository()
-    val ci_jobs =
-      space_explode(',', options.string("build_manager_ci_jobs")).map(isabelle.CI_Build.the_job)
+    val ci_jobs = space_explode(',', options.string("build_manager_ci_jobs")).map(Build_CI.the_job)
 
     progress.echo_if(ci_jobs.nonEmpty, "Managing ci jobs: " + commas_quote(ci_jobs.map(_.name)))