src/Pure/Concurrent/event_timer.scala
author wenzelm
Wed Oct 05 19:45:36 2016 +0200 (2016-10-05)
changeset 64056 0edc966bee55
parent 56768 06388a5cfb7c
child 64370 865b39487b5d
permissions -rw-r--r--
more date and time operations from Java 8;
     1 /*  Title:      Pure/Concurrent/event_timer.scala
     2     Module:     PIDE
     3     Author:     Makarius
     4 
     5 Initiate event after given point in time.
     6 
     7 Note: events are run as synchronized action within a dedicated thread
     8 and should finish quickly without further ado.
     9 */
    10 
    11 package isabelle
    12 
    13 
    14 import java.util.{Timer, TimerTask, Date => JDate}
    15 
    16 
    17 object Event_Timer
    18 {
    19   private lazy val event_timer = new Timer("event_timer", true)
    20 
    21   final class Request private[Event_Timer](val time: Time, task: TimerTask)
    22   {
    23     def cancel: Boolean = task.cancel
    24   }
    25 
    26   def request(time: Time)(event: => Unit): Request =
    27   {
    28     val task = new TimerTask { def run { event } }
    29     event_timer.schedule(task, new JDate(time.ms))
    30     new Request(time, task)
    31   }
    32 }
    33