# HG changeset patch
# User wenzelm
# Date 1398682614 -7200
# Node ID 06388a5cfb7c493641e57e2e969bf899f4875fc2
# Parent  9b311dbd0f55544cbf834076c57ec335d53f4a6d
added Scala version of module Event_Timer;

diff -r 9b311dbd0f55 -r 06388a5cfb7c src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Mon Apr 28 00:54:31 2014 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Mon Apr 28 12:56:54 2014 +0200
@@ -9,9 +9,8 @@
 
 signature EVENT_TIMER =
 sig
-  type event = unit -> unit
   eqtype request
-  val request: Time.time -> event -> request
+  val request: Time.time -> (unit -> unit) -> request
   val cancel: request -> bool
   val shutdown: unit -> unit
   val future: Time.time -> unit future
@@ -20,11 +19,6 @@
 structure Event_Timer: EVENT_TIMER =
 struct
 
-(* type event *)
-
-type event = unit -> unit;
-
-
 (* type request *)
 
 val request_counter = Counter.make ();
@@ -35,7 +29,7 @@
 (* type requests *)
 
 structure Requests = Table(type key = Time.time val ord = Time.compare);
-type requests = (request * event) list Requests.table;
+type requests = (request * (unit -> unit)) list Requests.table;
 
 fun add_request time entry (requests: requests) =
   Requests.cons_list (time, entry) requests;
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)
+  }
+}
+
diff -r 9b311dbd0f55 -r 06388a5cfb7c src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Apr 28 00:54:31 2014 +0200
+++ b/src/Pure/build-jars	Mon Apr 28 12:56:54 2014 +0200
@@ -11,6 +11,7 @@
 declare -a SOURCES=(
   Concurrent/consumer_thread.scala
   Concurrent/counter.scala
+  Concurrent/event_timer.scala
   Concurrent/future.scala
   Concurrent/mailbox.scala
   Concurrent/simple_thread.scala