dynamic evaluation of time (e.g. via options);
authorwenzelm
Mon, 10 Sep 2012 21:15:46 +0200
changeset 49249 c763444b34ad
parent 49248 bff772033a97
child 49250 332ab3748350
dynamic evaluation of time (e.g. via options); proper setInitialDelay, not setDelay;
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()
         }
       }