support for repeated events;

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