equal
deleted
inserted
replaced
113 pos: Position.T, |
113 pos: Position.T, |
114 serial: serial}; |
114 serial: serial}; |
115 |
115 |
116 fun entry_markup def kind (name, {pos, theory_long_name, serial, ...}: entry) = |
116 fun entry_markup def kind (name, {pos, theory_long_name, serial, ...}: entry) = |
117 Position.make_entity_markup def serial kind (name, pos) |
117 Position.make_entity_markup def serial kind (name, pos) |
118 ||> not (#def def) ? cons (Markup.def_theoryN, theory_long_name); |
118 ||> not (#def def orelse theory_long_name = "") ? cons (Markup.def_theoryN, theory_long_name); |
119 |
119 |
120 fun print_entry_ref kind (name, entry) = |
120 fun print_entry_ref kind (name, entry) = |
121 quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name); |
121 quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name); |
122 |
122 |
123 fun err_dup kind entry1 entry2 pos = |
123 fun err_dup kind entry1 entry2 pos = |