--- a/src/Tools/jEdit/src/rendering.scala Mon Mar 03 10:59:33 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Mon Mar 03 11:37:06 2014 +0100
@@ -330,7 +330,8 @@
private def hyperlink_file(props: Properties.T): Option[PIDE.editor.Hyperlink] =
props match {
case Position.Def_Line_File(line, name) =>
- PIDE.editor.hyperlink_source_file(name, line)
+ val offset = Position.Def_Offset.unapply(props) getOrElse 0
+ PIDE.editor.hyperlink_source_file(name, line, offset)
case Position.Def_Id_Offset(id, offset) =>
PIDE.editor.hyperlink_command_id(snapshot, id, offset)
case _ => None