src/Pure/sign.ML
changeset 17343 098db1bc1e59
parent 17221 6cd180204582
child 17405 e4dc583a2d79
equal deleted inserted replaced
17342:92504e2f6c07 17343:098db1bc1e59
    72   val hide_classes_i: bool -> string list -> theory -> theory
    72   val hide_classes_i: bool -> string list -> theory -> theory
    73   val hide_types: bool -> xstring list -> theory -> theory
    73   val hide_types: bool -> xstring list -> theory -> theory
    74   val hide_types_i: bool -> string list -> theory -> theory
    74   val hide_types_i: bool -> string list -> theory -> theory
    75   val hide_consts: bool -> xstring list -> theory -> theory
    75   val hide_consts: bool -> xstring list -> theory -> theory
    76   val hide_consts_i: bool -> string list -> theory -> theory
    76   val hide_consts_i: bool -> string list -> theory -> theory
       
    77   val hide_names: bool -> string * xstring list -> theory -> theory
       
    78   val hide_names_i: bool -> string * string list -> theory -> theory
    77 end
    79 end
    78 
    80 
    79 signature SIGN =
    81 signature SIGN =
    80 sig
    82 sig
    81   type sg    (*obsolete*)
    83   type sg    (*obsolete*)
   854 val hide_types_i = map_tsig oo Type.hide_types;
   856 val hide_types_i = map_tsig oo Type.hide_types;
   855 fun hide_consts b xs thy =
   857 fun hide_consts b xs thy =
   856   thy |> map_consts (apfst (apfst (fold (NameSpace.hide b o intern_const thy) xs)));
   858   thy |> map_consts (apfst (apfst (fold (NameSpace.hide b o intern_const thy) xs)));
   857 val hide_consts_i = (map_consts o apfst o apfst) oo (fold o NameSpace.hide);
   859 val hide_consts_i = (map_consts o apfst o apfst) oo (fold o NameSpace.hide);
   858 
   860 
       
   861 local
       
   862 
       
   863 val kinds =
       
   864  [("class", (intern_class, can o certify_class, hide_classes_i)),
       
   865   ("type", (intern_type, declared_tyname, hide_types_i)),
       
   866   ("const", (intern_const, declared_const, hide_consts_i))];
       
   867 
       
   868 fun gen_hide int b (kind, xnames) thy =
       
   869   (case AList.lookup (op =) kinds kind of
       
   870     SOME (intern, check, hide) =>
       
   871       let
       
   872         val names = if int then map (intern thy) xnames else xnames;
       
   873         val bads = filter_out (check thy) names;
       
   874       in
       
   875         if null bads then hide b names thy
       
   876         else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
       
   877       end
       
   878   | NONE => error ("Bad name space specification: " ^ quote kind));
       
   879 
       
   880 in
       
   881 
       
   882 val hide_names = gen_hide true;
       
   883 val hide_names_i = gen_hide false;
       
   884 
   859 end;
   885 end;
       
   886 
       
   887 end;