src/Pure/Isar/isar_syn.ML
changeset 56005 4f4fc80b0613
parent 55997 9dc5ce83202c
child 56006 6a4dcaf53664
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Mar 09 17:07:45 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 09 17:08:31 2014 +0100
     1.3 @@ -231,17 +231,36 @@
     1.4            #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
     1.5  
     1.6  
     1.7 -(* name space entry path *)
     1.8 +(* hide names *)
     1.9 +
    1.10 +local
    1.11 +
    1.12 +fun hide_names command_spec what hide parse prep =
    1.13 +  Outer_Syntax.command command_spec ("hide " ^ what ^ " from name space")
    1.14 +    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
    1.15 +      (Toplevel.theory (fn thy =>
    1.16 +        let val ctxt = Proof_Context.init_global thy
    1.17 +        in fold (hide fully o prep ctxt) args thy end))));
    1.18 +
    1.19 +in
    1.20  
    1.21 -fun hide_names spec hide what =
    1.22 -  Outer_Syntax.command spec ("hide " ^ what ^ " from name space")
    1.23 -    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
    1.24 -      (Toplevel.theory o uncurry hide));
    1.25 +val _ =
    1.26 +  hide_names @{command_spec "hide_class"} "classes" Sign.hide_class Parse.class
    1.27 +    Proof_Context.read_class;
    1.28 +
    1.29 +val _ =
    1.30 +  hide_names @{command_spec "hide_type"} "types" Sign.hide_type Parse.type_const
    1.31 +    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
    1.32  
    1.33 -val _ = hide_names @{command_spec "hide_class"} Isar_Cmd.hide_class "classes";
    1.34 -val _ = hide_names @{command_spec "hide_type"} Isar_Cmd.hide_type "types";
    1.35 -val _ = hide_names @{command_spec "hide_const"} Isar_Cmd.hide_const "constants";
    1.36 -val _ = hide_names @{command_spec "hide_fact"} Isar_Cmd.hide_fact "facts";
    1.37 +val _ =
    1.38 +  hide_names @{command_spec "hide_const"} "constants" Sign.hide_const Parse.const
    1.39 +    ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
    1.40 +
    1.41 +val _ =
    1.42 +  hide_names @{command_spec "hide_fact"} "facts" Global_Theory.hide_fact
    1.43 +    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
    1.44 +
    1.45 +end;
    1.46  
    1.47  
    1.48  (* use ML text *)