diff -r bff772033a97 -r c763444b34ad src/Pure/System/swing_thread.scala --- 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() } }