54 case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) => |
54 case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) => |
55 new External_Hyperlink(begin, end, line, ref_file, ref_line) |
55 new External_Hyperlink(begin, end, line, ref_file, ref_line) |
56 case Command.RefInfo(_, _, Some(id), Some(offset)) => |
56 case Command.RefInfo(_, _, Some(id), Some(offset)) => |
57 Isabelle.session.lookup_entity(id) match { |
57 Isabelle.session.lookup_entity(id) match { |
58 case Some(ref_cmd: Command) => |
58 case Some(ref_cmd: Command) => |
59 new Internal_Hyperlink(begin, end, line, |
59 document.command_start(ref_cmd) match { |
60 model.to_current(document, ref_cmd.start(document) + offset - 1)) |
60 case Some(ref_cmd_start) => |
|
61 new Internal_Hyperlink(begin, end, line, |
|
62 model.to_current(document, ref_cmd_start + offset - 1)) |
|
63 case None => null // FIXME external ref |
|
64 } |
61 case _ => null |
65 case _ => null |
62 } |
66 } |
63 case _ => null |
67 case _ => null |
64 } |
68 } |
65 case None => null |
69 case None => null |