equal
deleted
inserted
replaced
81 theory_name: string, |
81 theory_name: string, |
82 pos: Position.T, |
82 pos: Position.T, |
83 id: serial}; |
83 id: serial}; |
84 |
84 |
85 fun entry_markup def kind (name, {pos, id, ...}: entry) = |
85 fun entry_markup def kind (name, {pos, id, ...}: entry) = |
86 let |
86 Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name); |
87 val props = |
|
88 if def then (Markup.defN, string_of_int id) :: Position.properties_of pos |
|
89 else (Markup.refN, string_of_int id) :: Position.def_properties_of pos; |
|
90 in Markup.properties props (Markup.entity kind name) end; |
|
91 |
87 |
92 fun print_entry def kind (name, entry) = |
88 fun print_entry def kind (name, entry) = |
93 quote (Markup.markup (entry_markup def kind (name, entry)) name); |
89 quote (Markup.markup (entry_markup def kind (name, entry)) name); |
94 |
90 |
95 fun err_dup kind entry1 entry2 = |
91 fun err_dup kind entry1 entry2 = |