diff -r 9b311dbd0f55 -r 06388a5cfb7c src/Pure/Concurrent/event_timer.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/event_timer.scala	Mon Apr 28 12:56:54 2014 +0200
@@ -0,0 +1,33 @@
+/*  Title:      Pure/Concurrent/event_timer.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Initiate event after given point in time.
+
+Note: events are run as synchronized action within a dedicated thread
+and should finish quickly without further ado.
+*/
+
+package isabelle
+
+
+import java.util.{Timer, TimerTask, Date}
+
+
+object Event_Timer
+{
+  private lazy val event_timer = new Timer("event_timer", true)
+
+  final class Request private[Event_Timer](val time: Time, task: TimerTask)
+  {
+    def cancel: Boolean = task.cancel
+  }
+
+  def request(time: Time)(event: => Unit): Request =
+  {
+    val task = new TimerTask { def run { event } }
+    event_timer.schedule(task, new Date(time.ms))
+    new Request(time, task)
+  }
+}
+