clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
authorwenzelm
Tue, 31 Oct 2023 17:01:19 +0100
changeset 78870 674362fd8c96
parent 78869 f464f6bc5809
child 78871 3b21101c5b6b
clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 31 16:49:03 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 31 17:01:19 2023 +0100
@@ -558,11 +558,16 @@
 
     /* structured tasks */
 
-    def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
-      for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "") run_now(task))
+    def SEQ(tasks: List[() => Option[Logger_Task]]): Logger_Task =
+      Logger_Task(body = _ =>
+        for {
+          t <- tasks.iterator
+          task <- t()
+          if !exclude_task(task.name) || task.name == ""
+        } run_now(task))
 
     def SEQUENTIAL(tasks: Logger_Task*): Logger_Task =
-      SEQ(tasks.toList)
+      SEQ(List.from(for (task <- tasks.iterator) yield () => Some(task)))
 
     def PAR(tasks: List[Logger_Task]): Logger_Task =
       Logger_Task(body =
@@ -615,15 +620,18 @@
                       snapshot = Some(Isabelle_Devel.build_log_snapshot))))),
             PAR(
               List(remote_builds1, remote_builds2).map(remote_builds =>
-              SEQUENTIAL(
-                PAR(remote_builds.map(_.filter(_.active())).map(seq =>
-                  SEQ(
-                    for {
-                      (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
-                      (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r))
-                    } yield remote_build_history(rev, afp_rev, i, r)))),
-                Logger_Task("build_status",
-                  logger => Isabelle_Devel.build_status(logger.options))))),
+                SEQUENTIAL(
+                  PAR(remote_builds.map(_.filter(_.active())).map(seq =>
+                    SEQ(
+                      for {
+                        (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
+                      } yield () => {
+                        r.pick(logger.options, hg.id(), history_base_filter(r))
+                          .map({ case (rev, afp_rev) => remote_build_history(rev, afp_rev, i, r) })
+                      }
+                    ))),
+                  Logger_Task("build_status",
+                    logger => Isabelle_Devel.build_status(logger.options))))),
             exit))))
 
     log_service.shutdown()