src/Tools/jEdit/src/jedit_lib.scala
changeset 55549 5c40782f68b3
parent 53786 064cb0458071
child 55690 d73949233c2e
     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        }