--- a/src/Pure/General/delay.scala Sat Jul 04 22:22:34 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-/* 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()
- }
- }
-}