# 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)
   }
 }