# 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)