# HG changeset patch # User wenzelm # Date 1698768079 -3600 # Node ID 674362fd8c96e30e93c5fa86e880d8ce34d75b93 # Parent f464f6bc5809cc36f7aa6e226797f66d46460562 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37); diff -r f464f6bc5809 -r 674362fd8c96 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()