clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;
--- a/src/Tools/jEdit/src/jedit_lib.scala Tue Feb 18 14:05:08 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Feb 18 15:38:50 2014 +0100
@@ -222,9 +222,10 @@
try {
val p = text_area.offsetToXY(range.start)
val (q, r) =
- if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
- else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
+ if (try_get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n"))
(text_area.offsetToXY(stop - 1), char_width)
+ else if (stop >= end)
+ (text_area.offsetToXY(end), char_width * (stop - end))
else (text_area.offsetToXY(stop), 0)
(p, q, r)
}