Delayed action.

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

--- 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