mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;

--- a/src/Pure/Concurrent/simple_thread.scala	Mon Apr 28 14:19:14 2014 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala	Mon Apr 28 14:41:49 2014 +0200
@@ -51,5 +51,58 @@
 
   def submit_task[A](body: => A): JFuture[A] =
     default_pool.submit(new Callable[A] { def call = body })
+
+
+  /* delayed events */
+
+  final class Delay private [Simple_Thread](first: Boolean, delay: => Time, event: => Unit)
+  {
+    private var running: Option[Event_Timer.Request] = None
+
+    private def run: Unit =
+    {
+      val do_run = synchronized {
+        if (running.isDefined) { running = None; true } else false
+      }
+      if (do_run) event
+    }
+
+    def invoke(): Unit = synchronized
+    {
+      val new_run =
+        running match {
+          case Some(request) => if (first) false else { request.cancel; true }
+          case None => true
+        }
+      if (new_run)
+        running = Some(Event_Timer.request(Time.now() + delay)(run))
+    }
+
+    def revoke(): Unit = synchronized
+    {
+      running match {
+        case Some(request) => request.cancel; running = None
+        case None =>
+      }
+    }
+
+    def postpone(alt_delay: Time): Unit =
+    {
+      running match {
+        case Some(request) =>
+          val alt_time = Time.now() + alt_delay
+          if (request.time < alt_time && request.cancel) {
+            running = Some(Event_Timer.request(alt_time)(run))
+          }
+        case None =>
+      }
+    }
+  }
+
+  // delayed event after first invocation
+  def delay_first(delay: => Time)(event: => Unit): Delay = new Delay(true, delay, event)
+
+  // delayed event after last invocation
+  def delay_last(delay: => Time)(event: => Unit): Delay = new Delay(false, delay, event)
 }
 

--- a/src/Pure/GUI/swing_thread.scala	Mon Apr 28 14:19:14 2014 +0200
+++ b/src/Pure/GUI/swing_thread.scala	Mon Apr 28 14:41:49 2014 +0200
@@ -54,53 +54,11 @@
   }
 
 
-  /* delayed actions */
-
-  abstract class Delay extends
-  {
-    def invoke(): Unit
-    def revoke(): Unit
-    def postpone(time: Time): Unit
-  }
-
-  private def delayed_action(first: Boolean)(time: => Time)(action: => Unit): Delay =
-    new Delay {
-      private val timer = new Timer(time.ms.toInt, null)
-      timer.setRepeats(false)
-      timer.addActionListener(new ActionListener {
-        override def actionPerformed(e: ActionEvent) {
-          assert {}
-          timer.setInitialDelay(time.ms.toInt)
-          action
-        }
-      })
+  /* delayed events */
 
-      def invoke()
-      {
-        require {}
-        if (first) timer.start() else timer.restart()
-      }
-
-      def revoke()
-      {
-        require {}
-        timer.stop()
-        timer.setInitialDelay(time.ms.toInt)
-      }
+  def delay_first(delay: => Time)(event: => Unit): Simple_Thread.Delay =
+    Simple_Thread.delay_first(delay) { later { event } }
 
-      def postpone(alt_time: Time)
-      {
-        require {}
-        if (timer.isRunning) {
-          timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
-          timer.restart()
-        }
-      }
-    }
-
-  // delayed action after first invocation
-  def delay_first = delayed_action(true) _
-
-  // delayed action after last invocation
-  def delay_last = delayed_action(false) _
+  def delay_last(delay: => Time)(event: => Unit): Simple_Thread.Delay =
+    Simple_Thread.delay_last(delay) { later { event } }
 }

--- a/src/Tools/jEdit/src/document_view.scala	Mon Apr 28 14:19:14 2014 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Apr 28 14:41:49 2014 +0200
@@ -196,9 +196,7 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Raw_Edits =>
-        Swing_Thread.later {
-          overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
-        }
+        overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
 
       case changed: Session.Commands_Changed =>
         val buffer = model.buffer
@@ -213,7 +211,7 @@
               if (changed.assignment || load_changed ||
                   (changed.nodes.contains(model.node_name) &&
                    changed.commands.exists(snapshot.node.commands.contains)))
-                Swing_Thread.later { overview.delay_repaint.invoke() }
+                overview.delay_repaint.invoke()
 
               val visible_lines = text_area.getVisibleLines
               if (visible_lines > 0) {

--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 28 14:19:14 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 28 14:41:49 2014 +0200
@@ -34,7 +34,7 @@
   private val delay_flush =
     Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
 
-  def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() }
+  def invoke(): Unit = delay_flush.invoke()
 
 
   /* current situation */

--- a/src/Tools/jEdit/src/monitor_dockable.scala	Mon Apr 28 14:19:14 2014 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Mon Apr 28 14:41:49 2014 +0200
@@ -19,15 +19,17 @@
 
 class Monitor_Dockable(view: View, position: String) extends Dockable(view, position)
 {
+  private val rev_stats = Synchronized(Nil: List[Properties.T])
+
+
   /* chart data -- owned by Swing thread */
 
   private val chart = ML_Statistics.empty.chart(null, Nil)
   private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
-  private var rev_stats: List[Properties.T] = Nil
 
   private val delay_update =
     Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
-      ML_Statistics("", rev_stats.reverse)
+      ML_Statistics("", rev_stats.value.reverse)
         .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
     }
 
@@ -39,10 +41,8 @@
   private val main =
     Session.Consumer[Session.Statistics](getClass.getName) {
       case stats =>
-        Swing_Thread.later {
-          rev_stats ::= stats.props
-          delay_update.invoke()
-        }
+        rev_stats.change(stats.props :: _)
+        delay_update.invoke()
     }
 
   override def init() { PIDE.session.statistics += main }

--- a/src/Tools/jEdit/src/plugin.scala	Mon Apr 28 14:19:14 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Apr 28 14:41:49 2014 +0200
@@ -173,12 +173,12 @@
   def options_changed()
   {
     PIDE.session.global_options.post(Session.Global_Options(PIDE.options.value))
-    Swing_Thread.later { delay_load.invoke() }
+    delay_load.invoke()
   }
 
   def deps_changed()
   {
-    Swing_Thread.later { delay_load.invoke() }
+    delay_load.invoke()
   }
 
 
@@ -255,11 +255,11 @@
       case Session.Ready =>
         PIDE.session.update_options(PIDE.options.value)
         PIDE.init_models()
-        Swing_Thread.later { delay_load.invoke() }
+        delay_load.invoke()
 
       case Session.Shutdown =>
         PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
-        Swing_Thread.later { delay_load.revoke() }
+        delay_load.revoke()
 
       case _ =>
     }

--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Apr 28 14:19:14 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Apr 28 14:41:49 2014 +0200
@@ -173,7 +173,7 @@
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
-    override def componentShown(e: ComponentEvent)   { delay_resize.invoke() }
+    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   })
 
 

--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Mon Apr 28 14:19:14 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Mon Apr 28 14:41:49 2014 +0200
@@ -198,7 +198,7 @@
 
   peer.addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
-    override def componentShown(e: ComponentEvent)   { delay_resize.invoke() }
+    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   })