src/Tools/jEdit/src/jedit_editor.scala
changeset 55822 ccf2d784be97
parent 55783 da0513d95155
child 55876 142139457653
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Mar 01 13:05:46 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Mar 01 15:58:47 2014 +0100
     1.3 @@ -156,7 +156,7 @@
     1.4    override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
     1.5      new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
     1.6  
     1.7 -  override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
     1.8 +  override def hyperlink_command(snapshot: Document.Snapshot, command: Command, raw_offset: Int = 0)
     1.9      : Option[Hyperlink] =
    1.10    {
    1.11      if (snapshot.is_outdated) None
    1.12 @@ -167,8 +167,8 @@
    1.13            val file_name = command.node_name.node
    1.14            val sources =
    1.15              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
    1.16 -              (if (offset == 0) Iterator.empty
    1.17 -               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
    1.18 +              (if (raw_offset == 0) Iterator.empty
    1.19 +               else Iterator.single(command.source(Text.Range(0, command.decode(raw_offset)))))
    1.20            val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
    1.21            Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
    1.22        }