# HG changeset patch # User wenzelm # Date 1398688909 -7200 # Node ID e160ae47db942709f93c3d064e9e4aae2e35428e # Parent 8649243d7e91a30c7177579eb99ec40d6fcde6ec mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later; diff -r 8649243d7e91 -r e160ae47db94 src/Pure/Concurrent/simple_thread.scala --- 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) } diff -r 8649243d7e91 -r e160ae47db94 src/Pure/GUI/swing_thread.scala --- 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 } } } diff -r 8649243d7e91 -r e160ae47db94 src/Tools/jEdit/src/document_view.scala --- 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) { diff -r 8649243d7e91 -r e160ae47db94 src/Tools/jEdit/src/jedit_editor.scala --- 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 */ diff -r 8649243d7e91 -r e160ae47db94 src/Tools/jEdit/src/monitor_dockable.scala --- 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 } diff -r 8649243d7e91 -r e160ae47db94 src/Tools/jEdit/src/plugin.scala --- 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 _ => } diff -r 8649243d7e91 -r e160ae47db94 src/Tools/jEdit/src/simplifier_trace_dockable.scala --- 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() } }) diff -r 8649243d7e91 -r e160ae47db94 src/Tools/jEdit/src/simplifier_trace_window.scala --- 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() } })