--- 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))
}