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