more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
authorwenzelm
Wed Mar 12 10:42:28 2014 +0100 (2014-03-12)
changeset 56057ad6bd8030d88
parent 56056 4d46d53566e6
child 56058 cd9ce893f2d6
more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
clarified sublocale_global: proper Local_Theory.exit (see also 8fe7414f00b1);
src/Pure/Isar/expression.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/toplevel.ML
src/Pure/sign.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Mar 11 22:49:28 2014 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Mar 12 10:42:28 2014 +0100
     1.3 @@ -944,9 +944,16 @@
     1.4  
     1.5  fun gen_sublocale_global prep_loc prep_interpretation
     1.6      before_exit raw_locale expression raw_eqns thy =
     1.7 -  thy
     1.8 -  |> Named_Target.init before_exit (prep_loc thy raw_locale)
     1.9 -  |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns;
    1.10 +  let
    1.11 +    val lthy = Named_Target.init before_exit (prep_loc thy raw_locale) thy;
    1.12 +    fun setup_proof after_qed =
    1.13 +      Element.witness_proof_eqs
    1.14 +        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
    1.15 +  in
    1.16 +    lthy |>
    1.17 +      generic_interpretation prep_interpretation setup_proof
    1.18 +        Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns
    1.19 +  end;
    1.20  
    1.21  in
    1.22  
     2.1 --- a/src/Pure/Isar/local_theory.ML	Tue Mar 11 22:49:28 2014 +0100
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Mar 12 10:42:28 2014 +0100
     2.3 @@ -65,7 +65,6 @@
     2.4    val exit_global: local_theory -> theory
     2.5    val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
     2.6    val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
     2.7 -  val perhaps_exit_global: Proof.context -> theory
     2.8  end;
     2.9  
    2.10  structure Local_Theory: LOCAL_THEORY =
    2.11 @@ -343,9 +342,4 @@
    2.12      val phi = standard_morphism lthy thy_ctxt;
    2.13    in (f phi x, thy) end;
    2.14  
    2.15 -fun perhaps_exit_global ctxt =
    2.16 -  if can assert ctxt
    2.17 -  then exit_global (assert_bottom true ctxt)
    2.18 -  else Proof_Context.theory_of ctxt;
    2.19 -
    2.20  end;
     3.1 --- a/src/Pure/Isar/toplevel.ML	Tue Mar 11 22:49:28 2014 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Mar 12 10:42:28 2014 +0100
     3.3 @@ -534,7 +534,7 @@
     3.4  
     3.5  fun theory_to_proof f = begin_proof
     3.6    (fn _ => fn gthy =>
     3.7 -    (Context.Theory o Sign.reset_group o Local_Theory.perhaps_exit_global,
     3.8 +    (Context.Theory o Sign.reset_group o Sign.change_check o Proof_Context.theory_of,
     3.9        (case gthy of
    3.10          Context.Theory thy => f (Sign.new_group thy)
    3.11        | _ => raise UNDEF)));
     4.1 --- a/src/Pure/sign.ML	Tue Mar 11 22:49:28 2014 +0100
     4.2 +++ b/src/Pure/sign.ML	Wed Mar 12 10:42:28 2014 +0100
     4.3 @@ -10,6 +10,7 @@
     4.4    val change_begin: theory -> theory
     4.5    val change_end: theory -> theory
     4.6    val change_end_local: Proof.context -> Proof.context
     4.7 +  val change_check: theory -> theory
     4.8    val syn_of: theory -> Syntax.syntax
     4.9    val tsig_of: theory -> Type.tsig
    4.10    val classes_of: theory -> Sorts.algebra
    4.11 @@ -165,6 +166,10 @@
    4.12  fun change_end_local ctxt =
    4.13    Context.raw_transfer (change_end (Proof_Context.theory_of ctxt)) ctxt;
    4.14  
    4.15 +fun change_check thy =
    4.16 +  if can change_end thy
    4.17 +  then raise Fail "Unfinished linear change of theory content" else thy;
    4.18 +
    4.19  
    4.20  (* syntax *)
    4.21  
     5.1 --- a/src/Pure/theory.ML	Tue Mar 11 22:49:28 2014 +0100
     5.2 +++ b/src/Pure/theory.ML	Wed Mar 12 10:42:28 2014 +0100
     5.3 @@ -175,7 +175,10 @@
     5.4      end;
     5.5  
     5.6  fun end_theory thy =
     5.7 -  thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;
     5.8 +  thy
     5.9 +  |> apply_wrappers (end_wrappers thy)
    5.10 +  |> Sign.change_check
    5.11 +  |> Context.finish_thy;
    5.12  
    5.13  
    5.14