--- 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 _
+ }
}