diff -r 3746a78a2c01 -r f5e9d182f645 src/Pure/GUI/swing_thread.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/swing_thread.scala	Sun Sep 22 14:30:34 2013 +0200
@@ -0,0 +1,104 @@
+/*  Title:      Pure/GUI/swing_thread.scala
+    Author:     Makarius
+
+Evaluation within the AWT/Swing thread.
+*/
+
+package isabelle
+
+import javax.swing.{SwingUtilities, Timer}
+import java.awt.event.{ActionListener, ActionEvent}
+
+
+object Swing_Thread
+{
+  /* checks */
+
+  def assert[A](body: => A) =
+  {
+    Predef.assert(SwingUtilities.isEventDispatchThread())
+    body
+  }
+
+  def require[A](body: => A) =
+  {
+    Predef.require(SwingUtilities.isEventDispatchThread())
+    body
+  }
+
+
+  /* main dispatch queue */
+
+  def now[A](body: => A): A =
+  {
+    if (SwingUtilities.isEventDispatchThread()) body
+    else {
+      lazy val result = { assert(); Exn.capture(body) }
+      SwingUtilities.invokeAndWait(new Runnable { def run = result })
+      Exn.release(result)
+    }
+  }
+
+  def future[A](body: => A): Future[A] =
+  {
+    if (SwingUtilities.isEventDispatchThread()) Future.value(body)
+    else Future.fork { now(body) }
+  }
+
+  def later(body: => Unit)
+  {
+    if (SwingUtilities.isEventDispatchThread()) body
+    else SwingUtilities.invokeLater(new Runnable { def run = body })
+  }
+
+
+  /* delayed actions */
+
+  abstract class Delay extends
+  {
+    def invoke(): Unit
+    def revoke(): Unit
+    def postpone(time: Time): Unit
+  }
+
+  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.setInitialDelay(time.ms.toInt)
+          action
+        }
+      })
+
+      def invoke()
+      {
+        require()
+        if (first) timer.start() else timer.restart()
+      }
+
+      def revoke()
+      {
+        require()
+        timer.stop()
+        timer.setInitialDelay(time.ms.toInt)
+      }
+
+      def postpone(alt_time: Time)
+      {
+        require()
+        if (timer.isRunning) {
+          timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
+          timer.restart()
+        }
+      }
+    }
+
+  // delayed action after first invocation
+  def delay_first = delayed_action(true) _
+
+  // delayed action after last invocation
+  def delay_last = delayed_action(false) _
+}