# HG changeset patch
# User wenzelm
# Date 1329834983 -3600
# Node ID edcccd7a9eee0df6f6a328a6f647543b9c301b81
# Parent  9c504481d27074da18ea08ea6b34da23c10539a8
overview.delay_repaint: avoid wasting GUI cycles via update_delay;
prefer delay_first for prover initiated events -- avoid indefinite delay;

diff -r 9c504481d270 -r edcccd7a9eee src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Feb 21 13:37:03 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Feb 21 15:36:23 2012 +0100
@@ -379,6 +379,9 @@
       super.removeNotify
     }
 
+    val delay_repaint =
+      Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }
+
     override def paintComponent(gfx: Graphics)
     {
       super.paintComponent(gfx)
@@ -442,7 +445,7 @@
             if (updated ||
                 (changed.nodes.contains(model.name) &&
                  changed.commands.exists(snapshot.node.commands.contains)))
-              overview.repaint()
+              overview.delay_repaint()
 
             if (updated) invalidate_range(visible)
             else {
diff -r 9c504481d270 -r edcccd7a9eee src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Feb 21 13:37:03 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Feb 21 15:36:23 2012 +0100
@@ -132,7 +132,7 @@
   /* resize */
 
   addComponentListener(new ComponentAdapter {
-    val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
+    val delay = Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
     override def componentResized(e: ComponentEvent) { delay() }
   })