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