src/Tools/jEdit/src/document_view.scala
changeset 56356 c3dbaa155ece
parent 56314 9a513737a0b2
child 56373 0605d90be6fc
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Apr 01 22:25:01 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Apr 01 23:04:22 2014 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4      val buffer_range = JEdit_Lib.buffer_range(model.buffer)
     1.5      val visible_lines =
     1.6        (for {
     1.7 -        i <- 0 until text_area.getVisibleLines
     1.8 +        i <- (0 until text_area.getVisibleLines).iterator
     1.9          start = text_area.getScreenLineStartOffset(i)
    1.10          stop = text_area.getScreenLineEndOffset(i)
    1.11          if start >= 0 && stop >= 0
    1.12 @@ -228,7 +228,7 @@
    1.13                        snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
    1.14                      if (visible_cmds.exists(changed.commands)) {
    1.15                        for {
    1.16 -                        line <- 0 until visible_lines
    1.17 +                        line <- (0 until visible_lines).iterator
    1.18                          start = text_area.getScreenLineStartOffset(line) if start >= 0
    1.19                          end = text_area.getScreenLineEndOffset(line) if end >= 0
    1.20                          range = Text.Range(start, end)