src/Tools/jEdit/src/utils/Delay.scala

added EventBus for new command- or keyword-declarations

/*
 * Delayed actions
 *
 * @author Fabian Immler, TU Munich
 */

package isabelle.utils

import javax.swing.Timer
import java.awt.event.{ActionListener, ActionEvent}

class Delay(amount : Int, action : () => Unit) {

  val timer : Timer = new Timer(amount, new ActionListener {
      override def actionPerformed(e:ActionEvent){
        action ()
      }
    })
  // if called very often, action is executed at most once
  // in amount milliseconds
  def delay_or_ignore () = {
    if (! timer.isRunning()){
      timer.setRepeats(false)
      timer.start()
    }
  }
}