1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Mar 17 17:36:10 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Mar 17 17:44:29 2012 +0100
     1.3 @@ -124,10 +124,10 @@
     1.4      Text.Perspective(
     1.5        for {
     1.6          i <- 0 until text_area.getVisibleLines
     1.7 -        val start = text_area.getScreenLineStartOffset(i)
     1.8 -        val stop = text_area.getScreenLineEndOffset(i)
     1.9 +        start = text_area.getScreenLineStartOffset(i)
    1.10 +        stop = text_area.getScreenLineEndOffset(i)
    1.11          if start >= 0 && stop >= 0
    1.12 -        val range <- buffer_range.try_restrict(Text.Range(start, stop))
    1.13 +        range <- buffer_range.try_restrict(Text.Range(start, stop))
    1.14          if !range.is_singularity
    1.15        }
    1.16        yield range)
    1.17 @@ -388,10 +388,10 @@
    1.18                        if (visible_cmds.exists(changed.commands)) {
    1.19                          for {
    1.20                            line <- 0 until text_area.getVisibleLines
    1.21 -                          val start = text_area.getScreenLineStartOffset(line) if start >= 0
    1.22 -                          val end = text_area.getScreenLineEndOffset(line) if end >= 0
    1.23 -                          val range = proper_line_range(start, end)
    1.24 -                          val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
    1.25 +                          start = text_area.getScreenLineStartOffset(line) if start >= 0
    1.26 +                          end = text_area.getScreenLineEndOffset(line) if end >= 0
    1.27 +                          range = proper_line_range(start, end)
    1.28 +                          line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
    1.29                            if line_cmds.exists(changed.commands)
    1.30                          } text_area.invalidateScreenLineRange(line, line)
    1.31                        }