added hide_names command (formerly Sign.hide_names), support fact name space;
authorwenzelm
Tue, 15 Apr 2008 18:49:26 +0200 (2008-04-15)
changeset 26671 c95590e01df5
parent 26670 11f1894911cb
child 26672 f99956db6ccd
added hide_names command (formerly Sign.hide_names), support fact name space;
src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Apr 15 18:49:25 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Apr 15 18:49:26 2008 +0200
@@ -22,6 +22,7 @@
   val declaration: string * Position.T -> local_theory -> local_theory
   val simproc_setup: string -> string list -> string * Position.T -> string list ->
     local_theory -> local_theory
+  val hide_names: bool -> string * xstring list -> theory -> theory
   val have: ((string * Attrib.src list) * (string * string list) list) list ->
     bool -> Proof.state -> Proof.state
   val hence: ((string * Attrib.src list) * (string * string list) list) list ->
@@ -252,6 +253,27 @@
   |> Context.proof_map;
 
 
+(* hide names *)
+
+val hide_kinds =
+ [("class", (Sign.intern_class, can o Sign.certify_class, Sign.hide_class)),
+  ("type", (Sign.intern_type, Sign.declared_tyname, Sign.hide_type)),
+  ("const", (Sign.intern_const, Sign.declared_const, Sign.hide_const)),
+  ("fact", (PureThy.intern_fact, PureThy.check_fact, PureThy.hide_fact))];
+
+fun hide_names b (kind, xnames) thy =
+  (case AList.lookup (op =) hide_kinds kind of
+    SOME (intern, check, hide) =>
+      let
+        val names = map (intern thy) xnames;
+        val bads = filter_out (check thy) names;
+      in
+        if null bads then fold (hide b) names thy
+        else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
+      end
+  | NONE => error ("Bad name space specification: " ^ quote kind));
+
+
 (* goals *)
 
 fun goal opt_chain goal stmt int =