src/Tools/jEdit/src/isabelle_hyperlinks.scala
changeset 44607 274eff0ea12e
parent 44582 479c07072992
child 44615 a4ff8a787202
     1.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Aug 31 14:39:41 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Aug 31 15:41:22 2011 +0200
     1.3 @@ -74,10 +74,10 @@
     1.4                      (props, props) match {
     1.5                        case (Position.Id(def_id), Position.Offset(def_offset)) =>
     1.6                          snapshot.state.find_command(snapshot.version, def_id) match {
     1.7 -                          case Some((def_name, def_node, def_cmd)) =>
     1.8 +                          case Some((def_node, def_cmd)) =>
     1.9                              def_node.command_start(def_cmd) match {
    1.10                                case Some(def_cmd_start) =>
    1.11 -                                new Internal_Hyperlink(def_name, begin, end, line,
    1.12 +                                new Internal_Hyperlink(def_cmd.node_name, begin, end, line,
    1.13                                    def_cmd_start + def_cmd.decode(def_offset))
    1.14                                case None => null
    1.15                              }