# HG changeset patch # User wenzelm # Date 1521300770 -3600 # Node ID f4a505d6bc94765aa83e648c4076d4e5e6ad4616 # Parent 5c438b774b4d69fb1f5172082595375ad1513e6c support for repeated events; diff -r 5c438b774b4d -r f4a505d6bc94 src/Pure/Concurrent/event_timer.scala --- a/src/Pure/Concurrent/event_timer.scala Sat Mar 17 16:24:59 2018 +0100 +++ b/src/Pure/Concurrent/event_timer.scala Sat Mar 17 16:32:50 2018 +0100 @@ -17,15 +17,18 @@ { private lazy val event_timer = new Timer("event_timer", true) - final class Request private[Event_Timer](val time: Time, task: TimerTask) + final class Request private[Event_Timer](val time: Time, val repeat: Option[Time], task: TimerTask) { def cancel: Boolean = task.cancel } - def request(time: Time)(event: => Unit): Request = + def request(time: Time, repeat: Option[Time] = None)(event: => Unit): Request = { val task = new TimerTask { def run { event } } - event_timer.schedule(task, new JDate(time.ms)) - new Request(time, task) + repeat match { + case None => event_timer.schedule(task, new JDate(time.ms)) + case Some(rep) => event_timer.schedule(task, new JDate(time.ms), rep.ms) + } + new Request(time, repeat, task) } }