198 (* name spaces *) |
198 (* name spaces *) |
199 |
199 |
200 fun global_path comment_ignore = PureThy.global_path; |
200 fun global_path comment_ignore = PureThy.global_path; |
201 fun local_path comment_ignore = PureThy.local_path; |
201 fun local_path comment_ignore = PureThy.local_path; |
202 |
202 |
203 fun gen_hide f ((kind, names), comment_ignore) thy = |
203 local |
204 if kind mem_string [Sign.classK, Sign.typeK, Sign.constK] then f (kind, names) thy |
204 |
205 else error ("Bad name space specification: " ^ quote kind); |
205 val kinds = |
206 |
206 [(Sign.classK, fn sg => fn c => c mem Sign.classes sg), |
207 fun hide_space x = gen_hide Theory.hide_space x; |
207 (Sign.typeK, fn sg => fn c => |
208 fun hide_space_i x = gen_hide Theory.hide_space_i x; |
208 let val {tycons, abbrs, ...} = Type.rep_tsig (Sign.tsig_of sg) |
|
209 in is_some (Symtab.lookup (tycons, c)) orelse is_some (Symtab.lookup (abbrs, c)) end), |
|
210 (Sign.constK, is_some oo Sign.const_type)]; |
|
211 |
|
212 fun gen_hide intern ((kind, xnames), comment_ignore) thy = |
|
213 (case assoc (kinds, kind) of |
|
214 Some check => |
|
215 let |
|
216 val sg = Theory.sign_of thy; |
|
217 val names = map (intern sg kind) xnames; |
|
218 val bads = filter_out (check sg) names; |
|
219 in |
|
220 if null bads then Theory.hide_space_i (kind, names) thy |
|
221 else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads) |
|
222 end |
|
223 | None => error ("Bad name space specification: " ^ quote kind)); |
|
224 |
|
225 in |
|
226 |
|
227 fun hide_space x = gen_hide Sign.intern x; |
|
228 fun hide_space_i x = gen_hide (K (K I)) x; |
|
229 |
|
230 end; |
209 |
231 |
210 |
232 |
211 (* signature and syntax *) |
233 (* signature and syntax *) |
212 |
234 |
213 val add_classes = Theory.add_classes o Comment.ignore; |
235 val add_classes = Theory.add_classes o Comment.ignore; |