support for repeated events;
authorwenzelm
Sat Mar 17 16:32:50 2018 +0100 (14 months ago)
changeset 67890f4a505d6bc94
parent 67889 5c438b774b4d
child 67891 4f383cd54f69
support for repeated events;
src/Pure/Concurrent/event_timer.scala
     1.1 --- a/src/Pure/Concurrent/event_timer.scala	Sat Mar 17 16:24:59 2018 +0100
     1.2 +++ b/src/Pure/Concurrent/event_timer.scala	Sat Mar 17 16:32:50 2018 +0100
     1.3 @@ -17,15 +17,18 @@
     1.4  {
     1.5    private lazy val event_timer = new Timer("event_timer", true)
     1.6  
     1.7 -  final class Request private[Event_Timer](val time: Time, task: TimerTask)
     1.8 +  final class Request private[Event_Timer](val time: Time, val repeat: Option[Time], task: TimerTask)
     1.9    {
    1.10      def cancel: Boolean = task.cancel
    1.11    }
    1.12  
    1.13 -  def request(time: Time)(event: => Unit): Request =
    1.14 +  def request(time: Time, repeat: Option[Time] = None)(event: => Unit): Request =
    1.15    {
    1.16      val task = new TimerTask { def run { event } }
    1.17 -    event_timer.schedule(task, new JDate(time.ms))
    1.18 -    new Request(time, task)
    1.19 +    repeat match {
    1.20 +      case None => event_timer.schedule(task, new JDate(time.ms))
    1.21 +      case Some(rep) => event_timer.schedule(task, new JDate(time.ms), rep.ms)
    1.22 +    }
    1.23 +    new Request(time, repeat, task)
    1.24    }
    1.25  }