overview.delay_repaint: avoid wasting GUI cycles via update_delay;
authorwenzelm
Tue, 21 Feb 2012 15:36:23 +0100
changeset 47442edcccd7a9eee
parent 47441 9c504481d270
child 47443 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
     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