src/Pure/System/swing_thread.scala

--- a/src/Pure/System/swing_thread.scala	Fri Sep 07 13:58:54 2012 +0200
+++ b/src/Pure/System/swing_thread.scala	Fri Sep 07 15:00:03 2012 +0200
@@ -51,6 +51,7 @@
   {
     def invoke(): Unit
     def revoke(): Unit
+    def postpone(time: Time): Unit
   }
 
   private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Delay =
@@ -77,6 +78,15 @@
         timer.stop()
         timer.setDelay(time.ms.toInt)
       }
+
+      def postpone(alt_time: Time)
+      {
+        require()
+        if (timer.isRunning) {
+          timer.setDelay(timer.getDelay max alt_time.ms.toInt)
+          timer.restart()
+        }
+      }
     }
 
   // delayed action after first invocation