# HG changeset patch
# User wenzelm
# Date 1330885445 -3600
# Node ID 6bccb1dc9bc34c616dd06ba87a32e20782b5f743
# Parent  d68ea01d5084aee9214c5167cfc35c5daae3c208
tuned comment;

diff -r d68ea01d5084 -r 6bccb1dc9bc3 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Sun Mar 04 19:16:09 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Sun Mar 04 19:24:05 2012 +0100
@@ -92,7 +92,7 @@
 
   /* visible text range */
 
-  // FIXME remove!?
+  // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
   def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
     Text.Range(start, end min model.buffer.getLength)