--- 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 =>
+ }
}
}
}