diff -r 642b6105e6f4 -r 7e119f32276a src/Tools/jEdit/src/jedit_editor.scala
--- 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 _ =>