close context elements via Expression.cert/read_declaration;
authorwenzelm
Tue Apr 03 18:22:14 2012 +0200 (2012-04-03)
changeset 473111addbe2a7458
parent 47310 610d9c212376
child 47312 344712917580
close context elements via Expression.cert/read_declaration;
ensure visible context;
src/HOL/Isar_Examples/Group_Context.thy
src/Pure/Isar/bundle.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/expression.ML
     1.1 --- a/src/HOL/Isar_Examples/Group_Context.thy	Tue Apr 03 17:48:16 2012 +0200
     1.2 +++ b/src/HOL/Isar_Examples/Group_Context.thy	Tue Apr 03 18:22:14 2012 +0200
     1.3 @@ -14,9 +14,9 @@
     1.4    fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "**" 70)
     1.5      and one :: "'a"
     1.6      and inverse :: "'a => 'a"
     1.7 -  assumes assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
     1.8 -    and left_one: "\<And>x. one ** x = x"
     1.9 -    and left_inverse: "\<And>x. inverse x ** x = one"
    1.10 +  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
    1.11 +    and left_one: "one ** x = x"
    1.12 +    and left_inverse: "inverse x ** x = one"
    1.13  begin
    1.14  
    1.15  text {* some consequences *}
     2.1 --- a/src/Pure/Isar/bundle.ML	Tue Apr 03 17:48:16 2012 +0200
     2.2 +++ b/src/Pure/Isar/bundle.ML	Tue Apr 03 18:22:14 2012 +0200
     2.3 @@ -91,10 +91,16 @@
     2.4    let val decls = maps (the_bundle ctxt o prep ctxt) args
     2.5    in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
     2.6  
     2.7 -fun gen_context prep_bundle prep_stmt raw_incls raw_elems gthy =
     2.8 +fun gen_context prep_bundle prep_decl raw_incls raw_elems gthy =
     2.9    let
    2.10      val lthy = Context.cases Named_Target.theory_init Local_Theory.assert gthy;
    2.11 -    val augment = gen_includes prep_bundle raw_incls #> prep_stmt raw_elems [] #> snd;
    2.12 +    fun augment ctxt =
    2.13 +      let
    2.14 +        val ((_, _, _, ctxt'), _) = ctxt
    2.15 +          |> Context_Position.set_visible true
    2.16 +          |> gen_includes prep_bundle raw_incls
    2.17 +          |> prep_decl ([], []) I raw_elems;
    2.18 +      in ctxt' |> Context_Position.restore_visible ctxt end;
    2.19    in
    2.20      (case gthy of
    2.21        Context.Theory _ => Local_Theory.target augment lthy |> Local_Theory.restore
    2.22 @@ -115,8 +121,8 @@
    2.23  fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
    2.24  fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
    2.25  
    2.26 -val context = gen_context (K I) Expression.cert_statement;
    2.27 -val context_cmd = gen_context check Expression.read_statement;
    2.28 +val context = gen_context (K I) Expression.cert_declaration;
    2.29 +val context_cmd = gen_context check Expression.read_declaration;
    2.30  
    2.31  end;
    2.32  
     3.1 --- a/src/Pure/Isar/class_declaration.ML	Tue Apr 03 17:48:16 2012 +0200
     3.2 +++ b/src/Pure/Isar/class_declaration.ML	Tue Apr 03 18:22:14 2012 +0200
     3.3 @@ -157,7 +157,7 @@
     3.4        fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
     3.5        #> Class.redeclare_operations thy sups
     3.6        #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
     3.7 -    val ((raw_supparams, _, raw_inferred_elems), _) =
     3.8 +    val ((raw_supparams, _, raw_inferred_elems, _), _) =
     3.9        Proof_Context.init_global thy
    3.10        |> Context.proof_map (Syntax_Phases.term_check 0 "after_infer_fixate" (K after_infer_fixate))
    3.11        |> prep_decl raw_supexpr init_class_body raw_elems;
    3.12 @@ -221,7 +221,7 @@
    3.13  
    3.14      (* process elements as class specification *)
    3.15      val class_ctxt = Class.begin sups base_sort thy_ctxt;
    3.16 -    val ((_, _, syntax_elems), _) = class_ctxt
    3.17 +    val ((_, _, syntax_elems, _), _) = class_ctxt
    3.18        |> Expression.cert_declaration supexpr I inferred_elems;
    3.19      fun check_vars e vs =
    3.20        if null vs then
     4.1 --- a/src/Pure/Isar/expression.ML	Tue Apr 03 17:48:16 2012 +0200
     4.2 +++ b/src/Pure/Isar/expression.ML	Tue Apr 03 18:22:14 2012 +0200
     4.3 @@ -21,14 +21,14 @@
     4.4    (* Declaring locales *)
     4.5    val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
     4.6      Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
     4.7 -      * Element.context_i list) * ((string * typ) list * Proof.context)
     4.8 +      * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
     4.9    val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
    4.10      Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
    4.11 -      * Element.context_i list) * ((string * typ) list * Proof.context)
    4.12 +      * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
    4.13        (*FIXME*)
    4.14    val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
    4.15      Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
    4.16 -      * Element.context_i list) * ((string * typ) list * Proof.context)
    4.17 +      * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
    4.18    val add_locale: (local_theory -> local_theory) -> binding -> binding ->
    4.19      expression_i -> Element.context_i list -> theory -> string * local_theory
    4.20    val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding ->
    4.21 @@ -458,10 +458,10 @@
    4.22      val context' = context |>
    4.23        fix_params fixed |>
    4.24        fold (Context.proof_map o Locale.activate_facts NONE) deps;
    4.25 -    val (elems', _) = context' |>
    4.26 +    val (elems', context'') = context' |>
    4.27        Proof_Context.set_stmt true |>
    4.28        fold_map activate elems;
    4.29 -  in ((fixed, deps, elems'), (parms, ctxt')) end;
    4.30 +  in ((fixed, deps, elems', context''), (parms, ctxt')) end;
    4.31  
    4.32  in
    4.33  
    4.34 @@ -735,7 +735,7 @@
    4.35      val _ = Locale.defined thy name andalso
    4.36        error ("Duplicate definition of locale " ^ quote name);
    4.37  
    4.38 -    val ((fixed, deps, body_elems), (parms, ctxt')) =
    4.39 +    val ((fixed, deps, body_elems, _), (parms, ctxt')) =
    4.40        prep_decl raw_import I raw_body (Proof_Context.init_global thy);
    4.41      val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
    4.42