use cycles in ci triggers;
authorFabian Huch <huch@in.tum.de>
Tue, 21 Jan 2025 11:12:44 +0100
changeset 81884 058f239b860a
parent 81883 7ce4a45fe4c2
child 81885 b1e1019a78e4
use cycles in ci triggers;
src/Pure/Build/build_ci.scala
--- 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
   }