overview.delay_repaint: avoid wasting GUI cycles via update_delay;
authorwenzelm
Tue, 21 Feb 2012 15:36:23 +0100
changeset 46571 edcccd7a9eee
parent 46570 9c504481d270
child 46572 3074685ab7ed
overview.delay_repaint: avoid wasting GUI cycles via update_delay; prefer delay_first for prover initiated events -- avoid indefinite delay;
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/output_dockable.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 {
--- 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() }
   })