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