--- a/src/Pure/Build/build_ci.scala Tue Jan 21 10:05:40 2025 +0100
+++ b/src/Pure/Build/build_ci.scala Tue Jan 21 11:12:44 2025 +0100
@@ -70,17 +70,11 @@
case object On_Commit extends Trigger
object Timed {
- def nightly(start_time: Time = Time.zero): Timed =
- Timed { (before, now) =>
- val start0 = before.midnight + start_time
- val start1 = now.midnight + start_time
- (before.time < start0.time && start0.time <= now.time) ||
- (before.time < start1.time && start1.time <= now.time)
- }
+ def nightly(start_time: Time = Time.zero): Timed = Timed(Date.Daily(start_time))
}
- case class Timed(in_interval: (Date, Date) => Boolean) extends Trigger {
- def next(before: Date, now: Date): Boolean = in_interval(before, now)
+ case class Timed(cycle: Date.Cycle) extends Trigger {
+ def next(previous: Date, now: Date): Boolean = cycle.next(previous).time < cycle.next(now).time
}