diff -r d3a94ae9936f -r 63466160ff27 src/Pure/General/swing_thread.scala
--- a/src/Pure/General/swing_thread.scala	Sat Jul 04 22:22:34 2009 +0200
+++ b/src/Pure/General/swing_thread.scala	Sat Jul 04 23:25:28 2009 +0200
@@ -1,15 +1,20 @@
 /*  Title:      Pure/General/swing_thread.scala
     Author:     Makarius
+    Author:     Fabian Immler, TU Munich
 
 Evaluation within the AWT/Swing thread.
 */
 
 package isabelle
 
-import javax.swing.SwingUtilities
+import javax.swing.{SwingUtilities, Timer}
+import java.awt.event.{ActionListener, ActionEvent}
+
 
 object Swing_Thread
 {
+  /* main dispatch queue */
+
   def now[A](body: => A): A = {
     var result: Option[A] = None
     if (SwingUtilities.isEventDispatchThread) { result = Some(body) }
@@ -21,4 +26,23 @@
     if (SwingUtilities.isEventDispatchThread) body
     else SwingUtilities.invokeLater(new Runnable { def run = body })
   }
+
+
+  /* delayed actions */
+
+  // turn multiple invocations into single action within time span
+  def delay(time_span: Int)(action: => Unit): () => Unit =
+  {
+    val listener =
+      new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
+    val timer = new Timer(time_span, listener)
+    def invoke()
+    {
+      if (!timer.isRunning()) {
+        timer.setRepeats(false)
+        timer.start()
+      }
+    }
+    invoke _
+  }
 }