dropped obscure and unused ad-hoc before_exit hook for named targets
authorhaftmann
Fri Jun 06 19:19:46 2014 +0200 (2014-06-06)
changeset 571812d13bf9ea77b
parent 57180 74c81a5b5a34
child 57182 79d43c510b84
dropped obscure and unused ad-hoc before_exit hook for named targets
src/Doc/Implementation/Local_Theory.thy
src/HOL/Statespace/state_space.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/named_target.ML
     1.1 --- a/src/Doc/Implementation/Local_Theory.thy	Fri Jun 06 12:36:06 2014 +0200
     1.2 +++ b/src/Doc/Implementation/Local_Theory.thy	Fri Jun 06 19:19:46 2014 +0200
     1.3 @@ -96,8 +96,7 @@
     1.4  text %mlref {*
     1.5    \begin{mldecls}
     1.6    @{index_ML_type local_theory: Proof.context} \\
     1.7 -  @{index_ML Named_Target.init: "(local_theory -> local_theory) ->
     1.8 -    string -> theory -> local_theory"} \\[1ex]
     1.9 +  @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
    1.10    @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
    1.11      local_theory -> (term * (string * thm)) * local_theory"} \\
    1.12    @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
    1.13 @@ -120,9 +119,7 @@
    1.14    non-empty name refers to a @{command locale} or @{command class}
    1.15    context (a fully-qualified internal name is expected here).  This is
    1.16    useful for experimentation --- normally the Isar toplevel already
    1.17 -  takes care to initialize the local theory context.  The given @{text
    1.18 -  "before_exit"} function is invoked before leaving the context; in
    1.19 -  most situations plain identity @{ML I} is sufficient.
    1.20 +  takes care to initialize the local theory context.
    1.21  
    1.22    \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
    1.23    lthy"} defines a local entity according to the specification that is
     2.1 --- a/src/HOL/Statespace/state_space.ML	Fri Jun 06 12:36:06 2014 +0200
     2.2 +++ b/src/HOL/Statespace/state_space.ML	Fri Jun 06 19:19:46 2014 +0200
     2.3 @@ -127,20 +127,20 @@
     2.4  
     2.5  fun prove_interpretation_in ctxt_tac (name, expr) thy =
     2.6     thy
     2.7 -   |> Expression.sublocale_global_cmd I (name, Position.none) (expression_no_pos expr) []
     2.8 +   |> Expression.sublocale_global_cmd (name, Position.none) (expression_no_pos expr) []
     2.9     |> Proof.global_terminal_proof
    2.10           ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE)
    2.11     |> Proof_Context.theory_of
    2.12  
    2.13  fun add_locale name expr elems thy =
    2.14    thy
    2.15 -  |> Expression.add_locale I (Binding.name name) (Binding.name name) expr elems
    2.16 +  |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
    2.17    |> snd
    2.18    |> Local_Theory.exit;
    2.19  
    2.20  fun add_locale_cmd name expr elems thy =
    2.21    thy
    2.22 -  |> Expression.add_locale_cmd I (Binding.name name) Binding.empty (expression_no_pos expr) elems
    2.23 +  |> Expression.add_locale_cmd (Binding.name name) Binding.empty (expression_no_pos expr) elems
    2.24    |> snd
    2.25    |> Local_Theory.exit;
    2.26  
    2.27 @@ -294,7 +294,7 @@
    2.28  
    2.29  fun add_declaration name decl thy =
    2.30    thy
    2.31 -  |> Named_Target.init I name
    2.32 +  |> Named_Target.init name
    2.33    |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy)
    2.34    |> Local_Theory.exit_global;
    2.35  
     3.1 --- a/src/Pure/Isar/class_declaration.ML	Fri Jun 06 12:36:06 2014 +0200
     3.2 +++ b/src/Pure/Isar/class_declaration.ML	Fri Jun 06 19:19:46 2014 +0200
     3.3 @@ -6,14 +6,14 @@
     3.4  
     3.5  signature CLASS_DECLARATION =
     3.6  sig
     3.7 -  val class: (local_theory -> local_theory) -> binding -> class list ->
     3.8 +  val class: binding -> class list ->
     3.9      Element.context_i list -> theory -> string * local_theory
    3.10 -  val class_cmd: (local_theory -> local_theory) -> binding -> xstring list ->
    3.11 +  val class_cmd: binding -> xstring list ->
    3.12      Element.context list -> theory -> string * local_theory
    3.13 -  val prove_subclass: (local_theory -> local_theory) -> tactic -> class ->
    3.14 +  val prove_subclass: tactic -> class ->
    3.15      local_theory -> local_theory
    3.16 -  val subclass: (local_theory -> local_theory) -> class -> local_theory -> Proof.state
    3.17 -  val subclass_cmd: (local_theory -> local_theory) -> xstring -> local_theory -> Proof.state
    3.18 +  val subclass: class -> local_theory -> Proof.state
    3.19 +  val subclass_cmd: xstring -> local_theory -> Proof.state
    3.20  end;
    3.21  
    3.22  structure Class_Declaration: CLASS_DECLARATION =
    3.23 @@ -306,7 +306,7 @@
    3.24      #> pair (param_map, params, assm_axiom)))
    3.25    end;
    3.26  
    3.27 -fun gen_class prep_class_spec before_exit b raw_supclasses raw_elems thy =
    3.28 +fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
    3.29    let
    3.30      val class = Sign.full_name thy b;
    3.31      val prefix = Binding.qualify true "class";
    3.32 @@ -314,7 +314,7 @@
    3.33        prep_class_spec thy raw_supclasses raw_elems;
    3.34    in
    3.35      thy
    3.36 -    |> Expression.add_locale I b (prefix b) supexpr elems
    3.37 +    |> Expression.add_locale b (prefix b) supexpr elems
    3.38      |> snd |> Local_Theory.exit_global
    3.39      |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
    3.40      |-> (fn (param_map, params, assm_axiom) =>
    3.41 @@ -325,7 +325,7 @@
    3.42      #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
    3.43      #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
    3.44      |> snd
    3.45 -    |> Named_Target.init before_exit class
    3.46 +    |> Named_Target.init class
    3.47      |> pair class
    3.48    end;
    3.49  
    3.50 @@ -342,7 +342,7 @@
    3.51  
    3.52  local
    3.53  
    3.54 -fun gen_subclass prep_class do_proof before_exit raw_sup lthy =
    3.55 +fun gen_subclass prep_class do_proof raw_sup lthy =
    3.56    let
    3.57      val thy = Proof_Context.theory_of lthy;
    3.58      val proto_sup = prep_class thy raw_sup;
    3.59 @@ -371,7 +371,7 @@
    3.60  
    3.61  in
    3.62  
    3.63 -fun prove_subclass before_exit tac = gen_subclass (K I) (tactic_proof tac) before_exit;
    3.64 +fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
    3.65  
    3.66  fun subclass x = gen_subclass (K I) user_proof x;
    3.67  fun subclass_cmd x =
     4.1 --- a/src/Pure/Isar/expression.ML	Fri Jun 06 12:36:06 2014 +0200
     4.2 +++ b/src/Pure/Isar/expression.ML	Fri Jun 06 19:19:46 2014 +0200
     4.3 @@ -31,9 +31,9 @@
     4.4    val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
     4.5      Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
     4.6        * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
     4.7 -  val add_locale: (local_theory -> local_theory) -> binding -> binding ->
     4.8 +  val add_locale: binding -> binding ->
     4.9      expression_i -> Element.context_i list -> theory -> string * local_theory
    4.10 -  val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding ->
    4.11 +  val add_locale_cmd: binding -> binding ->
    4.12      expression -> Element.context list -> theory -> string * local_theory
    4.13  
    4.14    (* Interpretation *)
    4.15 @@ -53,9 +53,9 @@
    4.16      local_theory -> Proof.state
    4.17    val sublocale: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    4.18    val sublocale_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
    4.19 -  val sublocale_global: (local_theory -> local_theory) -> string -> expression_i ->
    4.20 +  val sublocale_global: string -> expression_i ->
    4.21      (Attrib.binding * term) list -> theory -> Proof.state
    4.22 -  val sublocale_global_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
    4.23 +  val sublocale_global_cmd: xstring * Position.T -> expression ->
    4.24      (Attrib.binding * string) list -> theory -> Proof.state
    4.25  
    4.26    (* Diagnostic *)
    4.27 @@ -762,7 +762,7 @@
    4.28    | defines_to_notes _ e = e;
    4.29  
    4.30  fun gen_add_locale prep_decl
    4.31 -    before_exit binding raw_predicate_binding raw_import raw_body thy =
    4.32 +    binding raw_predicate_binding raw_import raw_body thy =
    4.33    let
    4.34      val name = Sign.full_name thy binding;
    4.35      val _ = Locale.defined thy name andalso
    4.36 @@ -820,7 +820,7 @@
    4.37      val loc_ctxt = thy'
    4.38        |> Locale.register_locale binding (extraTs, params)
    4.39            (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
    4.40 -      |> Named_Target.init before_exit name
    4.41 +      |> Named_Target.init name
    4.42        |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
    4.43  
    4.44    in (name, loc_ctxt) end;
    4.45 @@ -938,9 +938,9 @@
    4.46  (* special case: global sublocale command *)
    4.47  
    4.48  fun gen_sublocale_global prep_loc prep_interpretation
    4.49 -    before_exit raw_locale expression raw_eqns thy =
    4.50 +    raw_locale expression raw_eqns thy =
    4.51    let
    4.52 -    val lthy = Named_Target.init before_exit (prep_loc thy raw_locale) thy;
    4.53 +    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
    4.54      fun setup_proof after_qed =
    4.55        Element.witness_proof_eqs
    4.56          (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Jun 06 12:36:06 2014 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Jun 06 19:19:46 2014 +0200
     5.3 @@ -442,7 +442,7 @@
     5.4        Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
     5.5        >> (fn ((name, (expr, elems)), begin) =>
     5.6            Toplevel.begin_local_theory begin
     5.7 -            (Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));
     5.8 +            (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
     5.9  
    5.10  fun interpretation_args mandatory =
    5.11    Parse.!!! (Parse_Spec.locale_expression mandatory) --
    5.12 @@ -454,7 +454,7 @@
    5.13      "prove sublocale relation between a locale and a locale expression"
    5.14      ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
    5.15        interpretation_args false >> (fn (loc, (expr, equations)) =>
    5.16 -        Toplevel.theory_to_proof (Expression.sublocale_global_cmd I loc expr equations)))
    5.17 +        Toplevel.theory_to_proof (Expression.sublocale_global_cmd loc expr equations)))
    5.18      || interpretation_args false >> (fn (expr, equations) =>
    5.19          Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
    5.20  
    5.21 @@ -483,11 +483,11 @@
    5.22     (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
    5.23      >> (fn ((name, (supclasses, elems)), begin) =>
    5.24          Toplevel.begin_local_theory begin
    5.25 -          (Class_Declaration.class_cmd I name supclasses elems #> snd)));
    5.26 +          (Class_Declaration.class_cmd name supclasses elems #> snd)));
    5.27  
    5.28  val _ =
    5.29    Outer_Syntax.local_theory_to_proof @{command_spec "subclass"} "prove a subclass relation"
    5.30 -    (Parse.class >> Class_Declaration.subclass_cmd I);
    5.31 +    (Parse.class >> Class_Declaration.subclass_cmd);
    5.32  
    5.33  val _ =
    5.34    Outer_Syntax.command @{command_spec "instantiation"} "instantiate and prove type arity"
     6.1 --- a/src/Pure/Isar/named_target.ML	Fri Jun 06 12:36:06 2014 +0200
     6.2 +++ b/src/Pure/Isar/named_target.ML	Fri Jun 06 19:19:46 2014 +0200
     6.3 @@ -9,7 +9,7 @@
     6.4  sig
     6.5    val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
     6.6    val is_theory: local_theory -> bool
     6.7 -  val init: (local_theory -> local_theory) -> string -> theory -> local_theory
     6.8 +  val init: string -> theory -> local_theory
     6.9    val theory_init: theory -> local_theory
    6.10    val reinit: local_theory -> local_theory -> local_theory
    6.11    val context_cmd: xstring * Position.T -> theory -> local_theory
    6.12 @@ -21,17 +21,15 @@
    6.13  (* context data *)
    6.14  
    6.15  datatype target =
    6.16 -  Target of {target: string, is_locale: bool, is_class: bool,
    6.17 -    before_exit: local_theory -> local_theory};
    6.18 +  Target of {target: string, is_locale: bool, is_class: bool};
    6.19 +
    6.20 +fun make_target target is_locale is_class =
    6.21 +  Target {target = target, is_locale = is_locale, is_class = is_class};
    6.22  
    6.23 -fun make_target target is_locale is_class before_exit =
    6.24 -  Target {target = target, is_locale = is_locale, is_class = is_class,
    6.25 -    before_exit = before_exit};
    6.26 -
    6.27 -fun named_target _ "" before_exit = make_target "" false false before_exit
    6.28 -  | named_target thy target before_exit =
    6.29 +fun named_target _ "" = make_target "" false false
    6.30 +  | named_target thy target =
    6.31        if Locale.defined thy target
    6.32 -      then make_target target true (Class.is_class thy target) before_exit
    6.33 +      then make_target target true (Class.is_class thy target)
    6.34        else error ("No such locale: " ^ quote target);
    6.35  
    6.36  structure Data = Proof_Data
    6.37 @@ -141,9 +139,9 @@
    6.38    else if not is_class then Locale.init target
    6.39    else Class.init target;
    6.40  
    6.41 -fun init before_exit target thy =
    6.42 +fun init target thy =
    6.43    let
    6.44 -    val ta = named_target thy target before_exit;
    6.45 +    val ta = named_target thy target;
    6.46      val naming = Sign.naming_of thy
    6.47        |> Name_Space.mandatory_path (Long_Name.base_name target);
    6.48    in
    6.49 @@ -158,16 +156,16 @@
    6.50          declaration = declaration ta,
    6.51          subscription = subscription ta,
    6.52          pretty = pretty ta,
    6.53 -        exit = before_exit #> Local_Theory.target_of #> Sign.change_end_local}
    6.54 +        exit = Local_Theory.target_of #> Sign.change_end_local}
    6.55    end;
    6.56  
    6.57 -val theory_init = init I "";
    6.58 +val theory_init = init "";
    6.59  
    6.60  val reinit =
    6.61    Local_Theory.assert_bottom true #> Data.get #> the #>
    6.62 -  (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
    6.63 +  (fn Target {target, ...} => Local_Theory.exit_global #> init target);
    6.64  
    6.65  fun context_cmd ("-", _) thy = theory_init thy
    6.66 -  | context_cmd target thy = init I (Locale.check thy target) thy;
    6.67 +  | context_cmd target thy = init (Locale.check thy target) thy;
    6.68  
    6.69  end;