src/Tools/jEdit/src/isabelle_hyperlinks.scala
changeset 44615 a4ff8a787202
parent 44607 274eff0ea12e
child 45468 33e946d3f449
     1.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Sep 01 11:33:44 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Sep 01 13:34:45 2011 +0200
     1.3 @@ -77,7 +77,7 @@
     1.4                            case Some((def_node, def_cmd)) =>
     1.5                              def_node.command_start(def_cmd) match {
     1.6                                case Some(def_cmd_start) =>
     1.7 -                                new Internal_Hyperlink(def_cmd.node_name, begin, end, line,
     1.8 +                                new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
     1.9                                    def_cmd_start + def_cmd.decode(def_offset))
    1.10                                case None => null
    1.11                              }