# HG changeset patch
# User haftmann
# Date 1366708490 -7200
# Node ID f069c7d496ca2a9917f439397fa231b7d8c60f1e
# Parent  d504e349e951265965a47aa3a00ae2c1cf19c1b5
brittleness stamping for local theories

diff -r d504e349e951 -r f069c7d496ca src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Apr 23 11:14:50 2013 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue Apr 23 11:14:50 2013 +0200
@@ -14,6 +14,8 @@
   val restore: local_theory -> local_theory
   val level: Proof.context -> int
   val assert_bottom: bool -> local_theory -> local_theory
+  val mark_brittle: local_theory -> local_theory
+  val assert_nonbrittle: local_theory -> local_theory
   val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
     local_theory -> local_theory
   val close_target: local_theory -> local_theory
@@ -95,27 +97,27 @@
 
 structure Data = Proof_Data
 (
-  type T = lthy list;
-  fun init _ = [];
+  type T = lthy list * bool;
+  fun init _ = ([], false);
 );
 
 fun assert lthy =
-  if null (Data.get lthy) then error "Missing local theory context" else lthy;
+  if null (fst (Data.get lthy)) then error "Missing local theory context" else lthy;
 
-val get_last_lthy = List.last o Data.get o assert;
-val get_first_lthy = hd o Data.get o assert;
+val get_last_lthy = List.last o fst o Data.get o assert;
+val get_first_lthy = hd o fst o Data.get o assert;
 
 fun map_first_lthy f =
   assert #>
-  Data.map (fn {naming, operations, after_close, target} :: parents =>
+  (Data.map o apfst) (fn {naming, operations, after_close, target} :: parents =>
     make_lthy (f (naming, operations, after_close, target)) :: parents);
 
-fun restore lthy = #target (get_first_lthy lthy) |> Data.put (Data.get lthy);
+fun restore lthy = #target (get_first_lthy lthy) |> Data.put (fst (Data.get lthy), false);
 
 
 (* nested structure *)
 
-val level = length o Data.get;  (*1: main target at bottom, >= 2: nested context*)
+val level = length o fst o Data.get;  (*1: main target at bottom, >= 2: nested context*)
 
 fun assert_bottom b lthy =
   let
@@ -129,17 +131,17 @@
 
 fun open_target naming operations after_close target =
   assert target
-  |> Data.map (cons (make_lthy (naming, operations, after_close, target)));
+  |> (Data.map o apfst) (cons (make_lthy (naming, operations, after_close, target)));
 
 fun close_target lthy =
   let
     val _ = assert_bottom false lthy;
-    val {after_close, ...} :: rest = Data.get lthy;
-  in lthy |> Data.put rest |> restore |> after_close end;
+    val ({after_close, ...} :: rest, tainted) = Data.get lthy;
+  in lthy |> Data.put (rest, tainted) |> restore |> after_close end;
 
 fun map_contexts f lthy =
   let val n = level lthy in
-    lthy |> (Data.map o map_index) (fn (i, {naming, operations, after_close, target}) =>
+    lthy |> (Data.map o apfst o map_index) (fn (i, {naming, operations, after_close, target}) =>
       make_lthy (naming, operations, after_close,
         target
         |> Context_Position.set_visible false
@@ -149,6 +151,16 @@
   end;
 
 
+(* brittle context -- implicit for nested structures *)
+
+val mark_brittle = Data.map (fn ([data], _) => ([data], true) | x => x);
+
+fun assert_nonbrittle lthy =
+  if snd (Data.get lthy) orelse level lthy > 1
+  then error "Brittle local theory context"
+  else lthy;
+
+
 (* naming *)
 
 val naming_of = #naming o get_first_lthy;
@@ -290,7 +302,7 @@
 (* init *)
 
 fun init naming operations target =
-  target |> Data.map
+  target |> (Data.map o apfst)
     (fn [] => [make_lthy (naming, operations, I, target)]
       | _ => error "Local theory already initialized")
   |> checkpoint;
diff -r d504e349e951 -r f069c7d496ca src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Apr 23 11:14:50 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Apr 23 11:14:50 2013 +0200
@@ -110,7 +110,7 @@
 (* local theory wrappers *)
 
 val loc_init = Named_Target.context_cmd;
-val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
+val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.assert_nonbrittle #> Local_Theory.exit_global;
 
 fun loc_begin loc (Context.Theory thy) =
       (Context.Theory o loc_exit, loc_init (the_default ("-", Position.none) loc) thy)