# HG changeset patch # User wenzelm # Date 1246738954 -7200 # Node ID d3a94ae9936f4a32687044967d55e2e75a50d14e # Parent 5fe21cac6bf7099e890d74e36cefc509c45261a9 Delayed action. diff -r 5fe21cac6bf7 -r d3a94ae9936f src/Pure/General/delay.scala --- /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() + } + } +} diff -r 5fe21cac6bf7 -r d3a94ae9936f src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sat Jul 04 12:40:57 2009 +0200 +++ b/src/Pure/IsaMakefile Sat Jul 04 22:22:34 2009 +0200 @@ -117,11 +117,11 @@ ## Scala material -SCALA_FILES = General/event_bus.scala General/markup.scala \ - General/position.scala General/scan.scala General/swing_thread.scala \ - General/symbol.scala General/xml.scala General/yxml.scala \ - Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala \ - System/cygwin.scala System/gui_setup.scala \ +SCALA_FILES = General/delay.scala General/event_bus.scala \ + General/markup.scala General/position.scala General/scan.scala \ + General/swing_thread.scala General/symbol.scala General/xml.scala \ + General/yxml.scala Isar/isar.scala Isar/isar_document.scala \ + Isar/outer_keyword.scala System/cygwin.scala System/gui_setup.scala \ System/isabelle_process.scala System/isabelle_system.scala \ System/platform.scala Thy/completion.scala Thy/thy_header.scala \ Tools/isabelle_syntax.scala