src/Pure/General/delay.scala

Delayed action.

/*  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()
    }
  }
}