# HG changeset patch
# User wenzelm
# Date 1394617348 -3600
# Node ID ad6bd8030d88efdfd3cd55280dcc8fb363a9d8b2
# Parent  4d46d53566e654db3ce8a2d61bc7120f2c842282
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);

diff -r 4d46d53566e6 -r ad6bd8030d88 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Mar 11 22:49:28 2014 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Mar 12 10:42:28 2014 +0100
@@ -944,9 +944,16 @@
 
 fun gen_sublocale_global prep_loc prep_interpretation
     before_exit raw_locale expression raw_eqns thy =
-  thy
-  |> Named_Target.init before_exit (prep_loc thy raw_locale)
-  |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns;
+  let
+    val lthy = Named_Target.init before_exit (prep_loc thy raw_locale) thy;
+    fun setup_proof after_qed =
+      Element.witness_proof_eqs
+        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
+  in
+    lthy |>
+      generic_interpretation prep_interpretation setup_proof
+        Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns
+  end;
 
 in
 
diff -r 4d46d53566e6 -r ad6bd8030d88 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Mar 11 22:49:28 2014 +0100
+++ b/src/Pure/Isar/local_theory.ML	Wed Mar 12 10:42:28 2014 +0100
@@ -65,7 +65,6 @@
   val exit_global: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
-  val perhaps_exit_global: Proof.context -> theory
 end;
 
 structure Local_Theory: LOCAL_THEORY =
@@ -343,9 +342,4 @@
     val phi = standard_morphism lthy thy_ctxt;
   in (f phi x, thy) end;
 
-fun perhaps_exit_global ctxt =
-  if can assert ctxt
-  then exit_global (assert_bottom true ctxt)
-  else Proof_Context.theory_of ctxt;
-
 end;
diff -r 4d46d53566e6 -r ad6bd8030d88 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Mar 11 22:49:28 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Mar 12 10:42:28 2014 +0100
@@ -534,7 +534,7 @@
 
 fun theory_to_proof f = begin_proof
   (fn _ => fn gthy =>
-    (Context.Theory o Sign.reset_group o Local_Theory.perhaps_exit_global,
+    (Context.Theory o Sign.reset_group o Sign.change_check o Proof_Context.theory_of,
       (case gthy of
         Context.Theory thy => f (Sign.new_group thy)
       | _ => raise UNDEF)));
diff -r 4d46d53566e6 -r ad6bd8030d88 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Mar 11 22:49:28 2014 +0100
+++ b/src/Pure/sign.ML	Wed Mar 12 10:42:28 2014 +0100
@@ -10,6 +10,7 @@
   val change_begin: theory -> theory
   val change_end: theory -> theory
   val change_end_local: Proof.context -> Proof.context
+  val change_check: theory -> theory
   val syn_of: theory -> Syntax.syntax
   val tsig_of: theory -> Type.tsig
   val classes_of: theory -> Sorts.algebra
@@ -165,6 +166,10 @@
 fun change_end_local ctxt =
   Context.raw_transfer (change_end (Proof_Context.theory_of ctxt)) ctxt;
 
+fun change_check thy =
+  if can change_end thy
+  then raise Fail "Unfinished linear change of theory content" else thy;
+
 
 (* syntax *)
 
diff -r 4d46d53566e6 -r ad6bd8030d88 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Mar 11 22:49:28 2014 +0100
+++ b/src/Pure/theory.ML	Wed Mar 12 10:42:28 2014 +0100
@@ -175,7 +175,10 @@
     end;
 
 fun end_theory thy =
-  thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;
+  thy
+  |> apply_wrappers (end_wrappers thy)
+  |> Sign.change_check
+  |> Context.finish_thy;