1/*  Title:      Pure/Concurrent/event_timer.scala
2    Author:     Makarius
3
4Initiate event after given point in time.
5
6Note: events are run as synchronized action within a dedicated thread
7and should finish quickly without further ado.
8*/
9
10package isabelle
11
12
13import java.util.{Timer, TimerTask, Date => JDate}
14
15
16object Event_Timer
17{
18  private lazy val event_timer = new Timer("event_timer", true)
19
20  final class Request private[Event_Timer](val time: Time, val repeat: Option[Time], task: TimerTask)
21  {
22    def cancel: Boolean = task.cancel
23  }
24
25  def request(time: Time, repeat: Option[Time] = None)(event: => Unit): Request =
26  {
27    val task = new TimerTask { def run { event } }
28    repeat match {
29      case None => event_timer.schedule(task, new JDate(time.ms))
30      case Some(rep) => event_timer.schedule(task, new JDate(time.ms), rep.ms)
31    }
32    new Request(time, repeat, task)
33  }
34}
35