equal
deleted
inserted
replaced
20 val select: ref -> thm list -> thm list |
20 val select: ref -> thm list -> thm list |
21 val selections: string * thm list -> (ref * thm) list |
21 val selections: string * thm list -> (ref * thm) list |
22 type T |
22 type T |
23 val empty: T |
23 val empty: T |
24 val space_of: T -> Name_Space.T |
24 val space_of: T -> Name_Space.T |
|
25 val alias: Name_Space.naming -> binding -> string -> T -> T |
25 val is_concealed: T -> string -> bool |
26 val is_concealed: T -> string -> bool |
26 val check: Context.generic -> T -> xstring * Position.T -> string |
27 val check: Context.generic -> T -> xstring * Position.T -> string |
27 val intern: T -> xstring -> string |
28 val intern: T -> xstring -> string |
28 val extern: Proof.context -> T -> string -> xstring |
29 val extern: Proof.context -> T -> string -> xstring |
29 val markup_extern: Proof.context -> T -> string -> Markup.T * xstring |
30 val markup_extern: Proof.context -> T -> string -> Markup.T * xstring |
141 |
142 |
142 fun facts_of (Facts {facts, ...}) = facts; |
143 fun facts_of (Facts {facts, ...}) = facts; |
143 |
144 |
144 val space_of = Name_Space.space_of_table o facts_of; |
145 val space_of = Name_Space.space_of_table o facts_of; |
145 |
146 |
|
147 fun alias naming binding name (Facts {facts, props}) = |
|
148 make_facts (Name_Space.alias_table naming binding name facts) props; |
|
149 |
146 val is_concealed = Name_Space.is_concealed o space_of; |
150 val is_concealed = Name_Space.is_concealed o space_of; |
147 |
151 |
148 fun check context facts (xname, pos) = |
152 fun check context facts (xname, pos) = |
149 let |
153 let |
150 val (name, fact) = Name_Space.check context (facts_of facts) (xname, pos); |
154 val (name, fact) = Name_Space.check context (facts_of facts) (xname, pos); |
154 | Dynamic _ => Context_Position.report_generic context pos (Markup.dynamic_fact name)); |
158 | Dynamic _ => Context_Position.report_generic context pos (Markup.dynamic_fact name)); |
155 in name end; |
159 in name end; |
156 |
160 |
157 val intern = Name_Space.intern o space_of; |
161 val intern = Name_Space.intern o space_of; |
158 fun extern ctxt = Name_Space.extern ctxt o space_of; |
162 fun extern ctxt = Name_Space.extern ctxt o space_of; |
159 fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of |
163 fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of; |
160 |
164 |
161 |
165 |
162 (* retrieve *) |
166 (* retrieve *) |
163 |
167 |
164 val defined = is_some oo (Name_Space.lookup_key o facts_of); |
168 val defined = is_some oo (Name_Space.lookup_key o facts_of); |