# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737454364 -3600
# Node ID 058f239b860a9b546edfbde14dc8a6e9cda0dd22
# Parent  7ce4a45fe4c265a7d986239a13af11115fd6bcf3
use cycles in ci triggers;

diff -r 7ce4a45fe4c2 -r 058f239b860a 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
   }