# 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;