changeset 57878 | 51a2f9140175 |
parent 57873 | ea94d2aa62be |
child 58545 | 30b75b7958d6 |
--- a/src/Tools/jEdit/src/jedit_editor.scala Sat Aug 09 18:50:39 2014 +0200 +++ b/src/Tools/jEdit/src/jedit_editor.scala Sun Aug 10 13:06:26 2014 +0200 @@ -246,7 +246,7 @@ def hyperlink_command_id( snapshot: Document.Snapshot, id: Document_ID.Generic, - offset: Symbol.Offset): Option[Hyperlink] = + offset: Symbol.Offset = 0): Option[Hyperlink] = { snapshot.state.find_command(snapshot.version, id) match { case Some((node, command)) => hyperlink_command(snapshot, command, offset)