src/Tools/jEdit/src/document_view.scala
changeset 49843 afddf4e26fac
parent 49492 2e3e7ea5ce8e
child 50199 6d04e2422769
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Oct 12 22:53:20 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Oct 12 23:38:48 2012 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4  
     1.5              for (i <- 0 until physical_lines.length) {
     1.6                if (physical_lines(i) != -1) {
     1.7 -                val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
     1.8 +                val line_range = Text.Range(start(i), end(i))
     1.9  
    1.10                  // gutter icons
    1.11                  rendering.gutter_message(line_range) match {
    1.12 @@ -201,7 +201,7 @@
    1.13                            line <- 0 until text_area.getVisibleLines
    1.14                            start = text_area.getScreenLineStartOffset(line) if start >= 0
    1.15                            end = text_area.getScreenLineEndOffset(line) if end >= 0
    1.16 -                          range = JEdit_Lib.proper_line_range(buffer, start, end)
    1.17 +                          range = Text.Range(start, end)
    1.18                            line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
    1.19                            if line_cmds.exists(changed.commands)
    1.20                          } text_area.invalidateScreenLineRange(line, line)