# HG changeset patch
# User wenzelm
# Date 1251922340 -7200
# Node ID 41aa620885c2a7fc09f3e04a4c812d6591424c18
# Parent  4ab2292e452af5a1e9adbce12e350ca66451210d
refined delay into delay_first/delay_last;

diff -r 4ab2292e452a -r 41aa620885c2 src/Pure/General/swing_thread.scala
--- a/src/Pure/General/swing_thread.scala	Wed Sep 02 20:49:04 2009 +0200
+++ b/src/Pure/General/swing_thread.scala	Wed Sep 02 22:12:20 2009 +0200
@@ -36,19 +36,20 @@
 
   /* delayed actions */
 
-  // turn multiple invocations into single action within time span
-  def delay(time_span: Int)(action: => Unit): () => Unit =
+  private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit =
   {
     val listener =
       new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
     val timer = new Timer(time_span, listener)
-    def invoke()
-    {
-      if (!timer.isRunning()) {
-        timer.setRepeats(false)
-        timer.start()
-      }
-    }
+    timer.setRepeats(false)
+
+    def invoke() { if (first) timer.start() else timer.restart() }
     invoke _
   }
+
+  // delayed action after first invocation
+  def delay_first = delayed_action(true) _
+
+  // delayed action after last invocation
+  def delay_last = delayed_action(false) _
 }