src/Tools/jEdit/src/document_view.scala
changeset 62986 9d2fae6b31cc
parent 62985 4be23c432491
child 63028 5fb352275db3
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Apr 14 20:47:44 2016 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Apr 14 22:55:53 2016 +0200
     1.3 @@ -185,6 +185,7 @@
     1.4    private val delay_caret_update =
     1.5      GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
     1.6        session.caret_focus.post(Session.Caret_Focus)
     1.7 +      JEdit_Lib.invalidate(text_area)
     1.8      }
     1.9  
    1.10    private val caret_listener = new CaretListener {
    1.11 @@ -219,26 +220,7 @@
    1.12                     changed.commands.exists(snapshot.node.commands.contains)))
    1.13                  text_overview.invoke()
    1.14  
    1.15 -              val visible_lines = text_area.getVisibleLines
    1.16 -              if (visible_lines > 0) {
    1.17 -                if (changed.assignment || load_changed)
    1.18 -                  text_area.invalidateScreenLineRange(0, visible_lines)
    1.19 -                else {
    1.20 -                  val visible_range = JEdit_Lib.visible_range(text_area).get
    1.21 -                  val visible_iterator =
    1.22 -                    snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
    1.23 -                  if (visible_iterator.exists(changed.commands)) {
    1.24 -                    for {
    1.25 -                      line <- (0 until visible_lines).iterator
    1.26 -                      start = text_area.getScreenLineStartOffset(line) if start >= 0
    1.27 -                      end = text_area.getScreenLineEndOffset(line) if end >= 0
    1.28 -                      range = Text.Range(start, end)
    1.29 -                      line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
    1.30 -                      if line_cmds.exists(changed.commands)
    1.31 -                    } text_area.invalidateScreenLineRange(line, line)
    1.32 -                  }
    1.33 -                }
    1.34 -              }
    1.35 +              JEdit_Lib.invalidate(text_area)
    1.36              }
    1.37            }
    1.38          }