--- a/src/Tools/jEdit/src/jedit/document_model.scala Fri Jun 25 14:05:49 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Sat Jun 26 21:26:35 2010 +0200
@@ -56,6 +56,19 @@
class Document_Model(val session: Session, val buffer: Buffer)
{
+ /* visible line end */
+
+ // simplify slightly odd result of TextArea.getLineEndOffset
+ // NB: jEdit already normalizes \r\n and \r to \n
+ def visible_line_end(start: Int, end: Int): Int =
+ {
+ val end1 = end - 1
+ if (start <= end1 && end1 < buffer.getLength &&
+ buffer.getSegment(end1, 1).charAt(0) == '\n') end1
+ else end
+ }
+
+
/* history */
private val document_0 = session.begin_document(buffer.getName)