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