renamed Delay to Swing_Thread.delay (action is executed within AWT thread!);

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

--- a/src/Pure/General/swing_thread.scala	Sat Jul 04 22:22:34 2009 +0200
+++ b/src/Pure/General/swing_thread.scala	Sat Jul 04 23:25:28 2009 +0200
@@ -1,15 +1,20 @@
 /*  Title:      Pure/General/swing_thread.scala
     Author:     Makarius
+    Author:     Fabian Immler, TU Munich
 
 Evaluation within the AWT/Swing thread.
 */
 
 package isabelle
 
-import javax.swing.SwingUtilities
+import javax.swing.{SwingUtilities, Timer}
+import java.awt.event.{ActionListener, ActionEvent}
+
 
 object Swing_Thread
 {
+  /* main dispatch queue */
+
   def now[A](body: => A): A = {
     var result: Option[A] = None
     if (SwingUtilities.isEventDispatchThread) { result = Some(body) }
@@ -21,4 +26,23 @@
     if (SwingUtilities.isEventDispatchThread) body
     else SwingUtilities.invokeLater(new Runnable { def run = body })
   }
+
+
+  /* delayed actions */
+
+  // turn multiple invocations into single action within time span
+  def delay(time_span: Int)(action: => Unit): () => Unit =
+  {
+    val listener =
+      new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
+    val timer = new Timer(time_span, listener)
+    def invoke()
+    {
+      if (!timer.isRunning()) {
+        timer.setRepeats(false)
+        timer.start()
+      }
+    }
+    invoke _
+  }
 }

--- a/src/Pure/IsaMakefile	Sat Jul 04 22:22:34 2009 +0200
+++ b/src/Pure/IsaMakefile	Sat Jul 04 23:25:28 2009 +0200
@@ -117,11 +117,11 @@
 
 ## Scala material
 
-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	\
+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				\
   System/isabelle_process.scala System/isabelle_system.scala		\
   System/platform.scala Thy/completion.scala Thy/thy_header.scala	\
   Tools/isabelle_syntax.scala