# HG changeset patch
# User wenzelm
# Date 1357647852 -3600
# Node ID 82d48783fd7ad6856e492ced5c2fafa83a9148cf
# Parent  41b54fd0619685565122a83227e1eef3a2d7eeea
more direct invalidateScreenLineRange after changed assignment;

diff -r 41b54fd06196 -r 82d48783fd7a src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Jan 08 12:50:57 2013 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Jan 08 13:24:12 2013 +0100
@@ -189,24 +189,24 @@
                      changed.commands.exists(snapshot.node.commands.contains)))
                   Swing_Thread.later { overview.delay_repaint.invoke() }
 
-                JEdit_Lib.visible_range(text_area) match {
-                  case Some(visible) =>
-                    if (changed.assignment) JEdit_Lib.invalidate_range(text_area, visible)
-                    else {
-                      val visible_cmds =
-                        snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
-                      if (visible_cmds.exists(changed.commands)) {
-                        for {
-                          line <- 0 until text_area.getVisibleLines
-                          start = text_area.getScreenLineStartOffset(line) if start >= 0
-                          end = text_area.getScreenLineEndOffset(line) if end >= 0
-                          range = Text.Range(start, end)
-                          line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
-                          if line_cmds.exists(changed.commands)
-                        } text_area.invalidateScreenLineRange(line, line)
-                      }
+                val visible_lines = text_area.getVisibleLines
+                if (visible_lines > 0) {
+                  if (changed.assignment) text_area.invalidateScreenLineRange(0, visible_lines)
+                  else {
+                    val visible_range = JEdit_Lib.visible_range(text_area).get
+                    val visible_cmds =
+                      snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
+                    if (visible_cmds.exists(changed.commands)) {
+                      for {
+                        line <- 0 until visible_lines
+                        start = text_area.getScreenLineStartOffset(line) if start >= 0
+                        end = text_area.getScreenLineEndOffset(line) if end >= 0
+                        range = Text.Range(start, end)
+                        line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+                        if line_cmds.exists(changed.commands)
+                      } text_area.invalidateScreenLineRange(line, line)
                     }
-                  case None =>
+                  }
                 }
               }
             }