dynamic evaluation of time (e.g. via options);
proper setInitialDelay, not setDelay;
--- a/src/Pure/System/swing_thread.scala Mon Sep 10 19:56:08 2012 +0200
+++ b/src/Pure/System/swing_thread.scala Mon Sep 10 21:15:46 2012 +0200
@@ -54,14 +54,14 @@
def postpone(time: Time): Unit
}
- private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Delay =
+ 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.setDelay(time.ms.toInt)
+ timer.setInitialDelay(time.ms.toInt)
action
}
})
@@ -76,14 +76,14 @@
{
require()
timer.stop()
- timer.setDelay(time.ms.toInt)
+ timer.setInitialDelay(time.ms.toInt)
}
def postpone(alt_time: Time)
{
require()
if (timer.isRunning) {
- timer.setDelay(timer.getDelay max alt_time.ms.toInt)
+ timer.setInitialDelay(timer.getDelay max alt_time.ms.toInt)
timer.restart()
}
}