src/Tools/jEdit/src/document_view.scala
changeset 55432 9c53198dbb1c
parent 54530 2c1440f70028
child 55618 995162143ef4
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Feb 11 17:44:29 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Feb 11 21:58:31 2014 +0100
     1.3 @@ -210,14 +210,18 @@
     1.4                if (model.buffer == text_area.getBuffer) {
     1.5                  val snapshot = model.snapshot()
     1.6  
     1.7 -                if (changed.assignment ||
     1.8 +                val thy_load_changed =
     1.9 +                  snapshot.thy_load_commands.exists(changed.commands.contains)
    1.10 +
    1.11 +                if (changed.assignment || thy_load_changed ||
    1.12                      (changed.nodes.contains(model.node_name) &&
    1.13                       changed.commands.exists(snapshot.node.commands.contains)))
    1.14                    Swing_Thread.later { overview.delay_repaint.invoke() }
    1.15  
    1.16                  val visible_lines = text_area.getVisibleLines
    1.17                  if (visible_lines > 0) {
    1.18 -                  if (changed.assignment) text_area.invalidateScreenLineRange(0, visible_lines)
    1.19 +                  if (changed.assignment || thy_load_changed)
    1.20 +                    text_area.invalidateScreenLineRange(0, visible_lines)
    1.21                    else {
    1.22                      val visible_range = JEdit_Lib.visible_range(text_area).get
    1.23                      val visible_cmds =