# HG changeset patch
# User wenzelm
# Date 1392734330 -3600
# Node ID 5c40782f68b3405df40ff6a969b2e454a3265574
# Parent  a645277885cf0dd59f5a9b46a2b1ea5c2875d527
clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;

diff -r a645277885cf -r 5c40782f68b3 src/Tools/jEdit/src/jedit_lib.scala
--- 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)
       }