src/Tools/jEdit/src/jedit_editor.scala
changeset 56462 b64b0cb845fe
parent 56461 ae33d153f6cc
child 56494 1b74abf064e1
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 08 10:24:42 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 08 12:19:33 2014 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4            val sources_iterator =
     1.5              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
     1.6                (if (offset == 0) Iterator.empty
     1.7 -               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
     1.8 +               else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
     1.9            val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
    1.10            Some(hyperlink_file(file_name, line, column))
    1.11        }