overview.delay_repaint: avoid wasting GUI cycles via update_delay;
prefer delay_first for prover initiated events -- avoid indefinite delay;
--- 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() }
})