equal
deleted
inserted
replaced
86 theory_name: string, |
86 theory_name: string, |
87 pos: Position.T, |
87 pos: Position.T, |
88 id: serial}; |
88 id: serial}; |
89 |
89 |
90 fun entry_markup def kind (name, {pos, id, ...}: entry) = |
90 fun entry_markup def kind (name, {pos, id, ...}: entry) = |
91 Markup.properties (Position.entity_properties_of def id pos) (Isabelle_Markup.entity kind name); |
91 Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name); |
92 |
92 |
93 fun print_entry_ref kind (name, entry) = |
93 fun print_entry_ref kind (name, entry) = |
94 quote (Markup.markup (entry_markup false kind (name, entry)) name); |
94 quote (Markup.markup (entry_markup false kind (name, entry)) name); |
95 |
95 |
96 fun err_dup kind entry1 entry2 pos = |
96 fun err_dup kind entry1 entry2 pos = |
131 |
131 |
132 fun entry_ord space = int_ord o pairself (#id o the_entry space); |
132 fun entry_ord space = int_ord o pairself (#id o the_entry space); |
133 |
133 |
134 fun markup (Name_Space {kind, entries, ...}) name = |
134 fun markup (Name_Space {kind, entries, ...}) name = |
135 (case Symtab.lookup entries name of |
135 (case Symtab.lookup entries name of |
136 NONE => Isabelle_Markup.intensify |
136 NONE => Markup.intensify |
137 | SOME (_, entry) => entry_markup false kind (name, entry)); |
137 | SOME (_, entry) => entry_markup false kind (name, entry)); |
138 |
138 |
139 fun is_concealed space name = #concealed (the_entry space name); |
139 fun is_concealed space name = #concealed (the_entry space name); |
140 |
140 |
141 |
141 |