--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/delay.scala Sat Jul 04 22:22:34 2009 +0200
@@ -0,0 +1,31 @@
+/* Title: Pure/General/symbol.scala
+ Author: Fabian Immler, TU Munich
+ Author: Makarius
+
+Delayed action: executed once after specified time span, even if
+prodded frequently.
+*/
+
+package isabelle
+
+import javax.swing.Timer
+import java.awt.event.{ActionListener, ActionEvent}
+
+
+object Delay
+{
+ def apply(amount: Int)(action: => Unit) = new Delay(amount)(action)
+}
+
+class Delay(amount: Int)(action: => Unit)
+{
+ private val timer = new Timer(amount,
+ new ActionListener { override def actionPerformed(e: ActionEvent) { action } })
+ def prod()
+ {
+ if (!timer.isRunning()) {
+ timer.setRepeats(false)
+ timer.start()
+ }
+ }
+}