equal
deleted
inserted
replaced
75 case (Position.Id(def_id), Position.Offset(def_offset)) => |
75 case (Position.Id(def_id), Position.Offset(def_offset)) => |
76 snapshot.state.find_command(snapshot.version, def_id) match { |
76 snapshot.state.find_command(snapshot.version, def_id) match { |
77 case Some((def_node, def_cmd)) => |
77 case Some((def_node, def_cmd)) => |
78 def_node.command_start(def_cmd) match { |
78 def_node.command_start(def_cmd) match { |
79 case Some(def_cmd_start) => |
79 case Some(def_cmd_start) => |
80 new Internal_Hyperlink(def_cmd.node_name, begin, end, line, |
80 new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line, |
81 def_cmd_start + def_cmd.decode(def_offset)) |
81 def_cmd_start + def_cmd.decode(def_offset)) |
82 case None => null |
82 case None => null |
83 } |
83 } |
84 case None => null |
84 case None => null |
85 } |
85 } |