src/Tools/jEdit/src/document_model.scala
changeset 65196 e8760a98db78
parent 65132 60e7072b8dbe
child 65243 ba5ce07e06a7
--- a/src/Tools/jEdit/src/document_model.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -338,7 +338,7 @@
 
   def node_position(offset: Text.Offset): Line.Node_Position =
     Line.Node_Position(node_name.node,
-      Line.Position.zero.advance(content.text.substring(0, offset), Text.Length))
+      Line.Position.zero.advance(content.text.substring(0, offset)))
 
   def get_blob: Option[Document.Blob] =
     if (is_theory) None