# HG changeset patch # User wenzelm # Date 1126642767 -7200 # Node ID 098db1bc1e59c65e71e9e2630072f3fa5fc8d943 # Parent 92504e2f6c07d13477bb36587206a3a1a38d8cd5 added hide_names(_i) (from isar_thy.ML); diff -r 92504e2f6c07 -r 098db1bc1e59 src/Pure/sign.ML --- a/src/Pure/sign.ML Tue Sep 13 22:19:26 2005 +0200 +++ b/src/Pure/sign.ML Tue Sep 13 22:19:27 2005 +0200 @@ -74,6 +74,8 @@ val hide_types_i: bool -> string list -> theory -> theory val hide_consts: bool -> xstring list -> theory -> theory val hide_consts_i: bool -> string list -> theory -> theory + val hide_names: bool -> string * xstring list -> theory -> theory + val hide_names_i: bool -> string * string list -> theory -> theory end signature SIGN = @@ -856,4 +858,30 @@ thy |> map_consts (apfst (apfst (fold (NameSpace.hide b o intern_const thy) xs))); val hide_consts_i = (map_consts o apfst o apfst) oo (fold o NameSpace.hide); +local + +val kinds = + [("class", (intern_class, can o certify_class, hide_classes_i)), + ("type", (intern_type, declared_tyname, hide_types_i)), + ("const", (intern_const, declared_const, hide_consts_i))]; + +fun gen_hide int b (kind, xnames) thy = + (case AList.lookup (op =) kinds kind of + SOME (intern, check, hide) => + let + val names = if int then map (intern thy) xnames else xnames; + val bads = filter_out (check thy) names; + in + if null bads then hide b names thy + else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads) + end + | NONE => error ("Bad name space specification: " ^ quote kind)); + +in + +val hide_names = gen_hide true; +val hide_names_i = gen_hide false; + end; + +end;