simplified / modernized hide commands: proper outer parsers and PIDE markup via check;
authorwenzelm
Sun Mar 09 17:08:31 2014 +0100 (2014-03-09)
changeset 560054f4fc80b0613
parent 56004 0364adabdc7b
child 56006 6a4dcaf53664
simplified / modernized hide commands: proper outer parsers and PIDE markup via check;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 09 17:07:45 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 09 17:08:31 2014 +0100
     1.3 @@ -21,10 +21,6 @@
     1.4      Symbol_Pos.source -> local_theory -> local_theory
     1.5    val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
     1.6      string list -> local_theory -> local_theory
     1.7 -  val hide_class: bool -> xstring list -> theory -> theory
     1.8 -  val hide_type: bool -> xstring list -> theory -> theory
     1.9 -  val hide_const: bool -> xstring list -> theory -> theory
    1.10 -  val hide_fact: bool -> xstring list -> theory -> theory
    1.11    val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    1.12    val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    1.13    val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    1.14 @@ -183,24 +179,6 @@
    1.15    |> Context.proof_map;
    1.16  
    1.17  
    1.18 -(* hide names *)
    1.19 -
    1.20 -fun hide_names intern check hide fully xnames thy =
    1.21 -  let
    1.22 -    val names = map (intern thy) xnames;
    1.23 -    val bads = filter_out (check thy) names;
    1.24 -  in
    1.25 -    if null bads then fold (hide fully) names thy
    1.26 -    else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
    1.27 -  end;
    1.28 -
    1.29 -val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class;
    1.30 -val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type;
    1.31 -val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const;
    1.32 -val hide_fact =
    1.33 -  hide_names Global_Theory.intern_fact Global_Theory.defined_fact Global_Theory.hide_fact;
    1.34 -
    1.35 -
    1.36  (* goals *)
    1.37  
    1.38  fun goal opt_chain goal stmt int =
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Mar 09 17:07:45 2014 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 09 17:08:31 2014 +0100
     2.3 @@ -231,17 +231,36 @@
     2.4            #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
     2.5  
     2.6  
     2.7 -(* name space entry path *)
     2.8 +(* hide names *)
     2.9 +
    2.10 +local
    2.11 +
    2.12 +fun hide_names command_spec what hide parse prep =
    2.13 +  Outer_Syntax.command command_spec ("hide " ^ what ^ " from name space")
    2.14 +    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
    2.15 +      (Toplevel.theory (fn thy =>
    2.16 +        let val ctxt = Proof_Context.init_global thy
    2.17 +        in fold (hide fully o prep ctxt) args thy end))));
    2.18 +
    2.19 +in
    2.20  
    2.21 -fun hide_names spec hide what =
    2.22 -  Outer_Syntax.command spec ("hide " ^ what ^ " from name space")
    2.23 -    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
    2.24 -      (Toplevel.theory o uncurry hide));
    2.25 +val _ =
    2.26 +  hide_names @{command_spec "hide_class"} "classes" Sign.hide_class Parse.class
    2.27 +    Proof_Context.read_class;
    2.28 +
    2.29 +val _ =
    2.30 +  hide_names @{command_spec "hide_type"} "types" Sign.hide_type Parse.type_const
    2.31 +    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
    2.32  
    2.33 -val _ = hide_names @{command_spec "hide_class"} Isar_Cmd.hide_class "classes";
    2.34 -val _ = hide_names @{command_spec "hide_type"} Isar_Cmd.hide_type "types";
    2.35 -val _ = hide_names @{command_spec "hide_const"} Isar_Cmd.hide_const "constants";
    2.36 -val _ = hide_names @{command_spec "hide_fact"} Isar_Cmd.hide_fact "facts";
    2.37 +val _ =
    2.38 +  hide_names @{command_spec "hide_const"} "constants" Sign.hide_const Parse.const
    2.39 +    ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
    2.40 +
    2.41 +val _ =
    2.42 +  hide_names @{command_spec "hide_fact"} "facts" Global_Theory.hide_fact
    2.43 +    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
    2.44 +
    2.45 +end;
    2.46  
    2.47  
    2.48  (* use ML text *)