clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;
authorwenzelm
Tue Feb 18 15:38:50 2014 +0100 (2014-02-18)
changeset 555495c40782f68b3
parent 55548 a645277885cf
child 55550 bcc643ac071a
clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Feb 18 14:05:08 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Feb 18 15:38:50 2014 +0100
     1.3 @@ -222,9 +222,10 @@
     1.4        try {
     1.5          val p = text_area.offsetToXY(range.start)
     1.6          val (q, r) =
     1.7 -          if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
     1.8 -          else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
     1.9 +          if (try_get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n"))
    1.10              (text_area.offsetToXY(stop - 1), char_width)
    1.11 +          else if (stop >= end)
    1.12 +            (text_area.offsetToXY(end), char_width * (stop - end))
    1.13            else (text_area.offsetToXY(stop), 0)
    1.14          (p, q, r)
    1.15        }