--- a/src/Tools/jEdit/src/jedit_editor.scala Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Wed Dec 28 17:10:09 2016 +0100
@@ -270,7 +270,8 @@
JEdit_Lib.buffer_lock(buffer) {
(Line.Position.zero /:
(Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
- zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_, Length))
+ zipWithIndex.takeWhile(p => p._2 < offset - 1).
+ map(_._1)))(_.advance(_, Text.Length))
}
hyperlink_file(focus, Line.Node_Position(name, pos))
case _ =>