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