--- 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 } }
}