# HG changeset patch
# User wenzelm
# Date 1442687517 -7200
# Node ID e4699ef5cf908b723ae9e62b042e19120571c08b
# Parent  dde5ecbd5e10f6ed920eef8d2ea296b198593916
allow to cancel running event;
synchronized postpone operation;

diff -r dde5ecbd5e10 -r e4699ef5cf90 src/Pure/Concurrent/simple_thread.scala
--- a/src/Pure/Concurrent/simple_thread.scala	Sat Sep 19 19:40:09 2015 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala	Sat Sep 19 20:31:57 2015 +0200
@@ -53,7 +53,8 @@
 
   /* delayed events */
 
-  final class Delay private [Simple_Thread](first: Boolean, delay: => Time, event: => Unit)
+  final class Delay private [Simple_Thread](
+    first: Boolean, delay: => Time, cancel: () => Unit, event: => Unit)
   {
     private var running: Option[Event_Timer.Request] = None
 
@@ -69,7 +70,7 @@
     {
       val new_run =
         running match {
-          case Some(request) => if (first) false else { request.cancel; true }
+          case Some(request) => if (first) false else { request.cancel; cancel(); true }
           case None => true
         }
       if (new_run)
@@ -79,28 +80,31 @@
     def revoke(): Unit = synchronized
     {
       running match {
-        case Some(request) => request.cancel; running = None
-        case None =>
+        case Some(request) => request.cancel; cancel(); running = None
+        case None => cancel()
       }
     }
 
-    def postpone(alt_delay: Time): Unit =
+    def postpone(alt_delay: Time): Unit = synchronized
     {
       running match {
         case Some(request) =>
           val alt_time = Time.now() + alt_delay
           if (request.time < alt_time && request.cancel) {
+            cancel()
             running = Some(Event_Timer.request(alt_time)(run))
           }
-        case None =>
+          else cancel()
+        case None => cancel()
       }
     }
   }
 
   // delayed event after first invocation
-  def delay_first(delay: => Time)(event: => Unit): Delay = new Delay(true, delay, event)
+  def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
+    new Delay(true, delay, cancel, event)
 
   // delayed event after last invocation
-  def delay_last(delay: => Time)(event: => Unit): Delay = new Delay(false, delay, event)
+  def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
+    new Delay(false, delay, cancel, event)
 }
-
diff -r dde5ecbd5e10 -r e4699ef5cf90 src/Pure/GUI/gui_thread.scala
--- a/src/Pure/GUI/gui_thread.scala	Sat Sep 19 19:40:09 2015 +0200
+++ b/src/Pure/GUI/gui_thread.scala	Sat Sep 19 20:31:57 2015 +0200
@@ -49,9 +49,9 @@
 
   /* delayed events */
 
-  def delay_first(delay: => Time)(event: => Unit): Simple_Thread.Delay =
-    Simple_Thread.delay_first(delay) { later { event } }
+  def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
+    : Simple_Thread.Delay = Simple_Thread.delay_first(delay, cancel) { later { event } }
 
-  def delay_last(delay: => Time)(event: => Unit): Simple_Thread.Delay =
-    Simple_Thread.delay_last(delay) { later { event } }
+  def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
+    : Simple_Thread.Delay = Simple_Thread.delay_last(delay, cancel) { later { event } }
 }