1.1 --- a/src/Tools/jEdit/src/document_view.scala Tue Feb 21 13:37:03 2012 +0100
1.2 +++ b/src/Tools/jEdit/src/document_view.scala Tue Feb 21 15:36:23 2012 +0100
1.3 @@ -379,6 +379,9 @@
1.4 super.removeNotify
1.5 }
1.6
1.7 + val delay_repaint =
1.8 + Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }
1.9 +
1.10 override def paintComponent(gfx: Graphics)
1.11 {
1.12 super.paintComponent(gfx)
1.13 @@ -442,7 +445,7 @@
1.14 if (updated ||
1.15 (changed.nodes.contains(model.name) &&
1.16 changed.commands.exists(snapshot.node.commands.contains)))
1.17 - overview.repaint()
1.18 + overview.delay_repaint()
1.19
1.20 if (updated) invalidate_range(visible)
1.21 else {
2.1 --- a/src/Tools/jEdit/src/output_dockable.scala Tue Feb 21 13:37:03 2012 +0100
2.2 +++ b/src/Tools/jEdit/src/output_dockable.scala Tue Feb 21 15:36:23 2012 +0100
2.3 @@ -132,7 +132,7 @@
2.4 /* resize */
2.5
2.6 addComponentListener(new ComponentAdapter {
2.7 - val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
2.8 + val delay = Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
2.9 override def componentResized(e: ComponentEvent) { delay() }
2.10 })
2.11