diff -r 8649243d7e91 -r e160ae47db94 src/Pure/GUI/swing_thread.scala
--- a/src/Pure/GUI/swing_thread.scala	Mon Apr 28 14:19:14 2014 +0200
+++ b/src/Pure/GUI/swing_thread.scala	Mon Apr 28 14:41:49 2014 +0200
@@ -54,53 +54,11 @@
   }
 
 
-  /* delayed actions */
-
-  abstract class Delay extends
-  {
-    def invoke(): Unit
-    def revoke(): Unit
-    def postpone(time: Time): Unit
-  }
-
-  private def delayed_action(first: Boolean)(time: => Time)(action: => Unit): Delay =
-    new Delay {
-      private val timer = new Timer(time.ms.toInt, null)
-      timer.setRepeats(false)
-      timer.addActionListener(new ActionListener {
-        override def actionPerformed(e: ActionEvent) {
-          assert {}
-          timer.setInitialDelay(time.ms.toInt)
-          action
-        }
-      })
+  /* delayed events */
 
-      def invoke()
-      {
-        require {}
-        if (first) timer.start() else timer.restart()
-      }
-
-      def revoke()
-      {
-        require {}
-        timer.stop()
-        timer.setInitialDelay(time.ms.toInt)
-      }
+  def delay_first(delay: => Time)(event: => Unit): Simple_Thread.Delay =
+    Simple_Thread.delay_first(delay) { later { event } }
 
-      def postpone(alt_time: Time)
-      {
-        require {}
-        if (timer.isRunning) {
-          timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
-          timer.restart()
-        }
-      }
-    }
-
-  // delayed action after first invocation
-  def delay_first = delayed_action(true) _
-
-  // delayed action after last invocation
-  def delay_last = delayed_action(false) _
+  def delay_last(delay: => Time)(event: => Unit): Simple_Thread.Delay =
+    Simple_Thread.delay_last(delay) { later { event } }
 }