mark local theory as brittle also after interpretation inside locales;
authorhaftmann
Wed May 22 22:56:17 2013 +0200 (2013-05-22)
changeset 521182a976115c7c3
parent 52117 352ea4b159ff
child 52119 90ba620333d0
mark local theory as brittle also after interpretation inside locales;
more correct bookkeeping on brittleness: must store directly beside lthy data, with implicit default true for levels > 1;
check brittleness only during context switch using (in ...) syntax, not for arbitrary exit of local theory
src/Pure/Isar/expression.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Wed May 22 19:44:51 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed May 22 22:56:17 2013 +0200
     1.3 @@ -879,8 +879,10 @@
     1.4      val is_theory = Option.map #target (Named_Target.peek lthy) = SOME ""
     1.5        andalso Local_Theory.level lthy = 1;
     1.6      val activate = if is_theory then add_registration else activate_local_theory;
     1.7 +    val mark_brittle = if is_theory then I else Local_Theory.mark_brittle;
     1.8    in
     1.9      lthy
    1.10 +    |> mark_brittle
    1.11      |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
    1.12          Local_Theory.notes_kind activate expression raw_eqns
    1.13    end;
     2.1 --- a/src/Pure/Isar/local_theory.ML	Wed May 22 19:44:51 2013 +0200
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Wed May 22 22:56:17 2013 +0200
     2.3 @@ -87,37 +87,38 @@
     2.4   {naming: Name_Space.naming,
     2.5    operations: operations,
     2.6    after_close: local_theory -> local_theory,
     2.7 +  brittle: bool,
     2.8    target: Proof.context};
     2.9  
    2.10 -fun make_lthy (naming, operations, after_close, target) : lthy =
    2.11 -  {naming = naming, operations = operations, after_close = after_close, target = target};
    2.12 +fun make_lthy (naming, operations, after_close, brittle, target) : lthy =
    2.13 +  {naming = naming, operations = operations, after_close = after_close, brittle = brittle, target = target};
    2.14  
    2.15  
    2.16  (* context data *)
    2.17  
    2.18  structure Data = Proof_Data
    2.19  (
    2.20 -  type T = lthy list * bool;
    2.21 -  fun init _ = ([], false);
    2.22 +  type T = lthy list;
    2.23 +  fun init _ = [];
    2.24  );
    2.25  
    2.26  fun assert lthy =
    2.27 -  if null (fst (Data.get lthy)) then error "Missing local theory context" else lthy;
    2.28 +  if null (Data.get lthy) then error "Missing local theory context" else lthy;
    2.29  
    2.30 -val get_last_lthy = List.last o fst o Data.get o assert;
    2.31 -val get_first_lthy = hd o fst o Data.get o assert;
    2.32 +val get_last_lthy = List.last o Data.get o assert;
    2.33 +val get_first_lthy = hd o Data.get o assert;
    2.34  
    2.35  fun map_first_lthy f =
    2.36    assert #>
    2.37 -  (Data.map o apfst) (fn {naming, operations, after_close, target} :: parents =>
    2.38 -    make_lthy (f (naming, operations, after_close, target)) :: parents);
    2.39 +  Data.map (fn {naming, operations, after_close, brittle, target} :: parents =>
    2.40 +    make_lthy (f (naming, operations, after_close, brittle, target)) :: parents);
    2.41  
    2.42 -fun restore lthy = #target (get_first_lthy lthy) |> Data.put (fst (Data.get lthy), false);
    2.43 +fun restore lthy = #target (get_first_lthy lthy) |> Data.put (Data.get lthy);
    2.44  
    2.45  
    2.46  (* nested structure *)
    2.47  
    2.48 -val level = length o fst o Data.get;  (*1: main target at bottom, >= 2: nested context*)
    2.49 +val level = length o Data.get;  (*1: main target at bottom, >= 2: nested context*)
    2.50  
    2.51  fun assert_bottom b lthy =
    2.52    let
    2.53 @@ -131,18 +132,18 @@
    2.54  
    2.55  fun open_target naming operations after_close target =
    2.56    assert target
    2.57 -  |> (Data.map o apfst) (cons (make_lthy (naming, operations, after_close, target)));
    2.58 +  |> Data.map (cons (make_lthy (naming, operations, after_close, true, target)));
    2.59  
    2.60  fun close_target lthy =
    2.61    let
    2.62      val _ = assert_bottom false lthy;
    2.63 -    val ({after_close, ...} :: rest, tainted) = Data.get lthy;
    2.64 -  in lthy |> Data.put (rest, tainted) |> restore |> after_close end;
    2.65 +    val ({after_close, ...} :: rest) = Data.get lthy;
    2.66 +  in lthy |> Data.put rest |> restore |> after_close end;
    2.67  
    2.68  fun map_contexts f lthy =
    2.69    let val n = level lthy in
    2.70 -    lthy |> (Data.map o apfst o map_index) (fn (i, {naming, operations, after_close, target}) =>
    2.71 -      make_lthy (naming, operations, after_close,
    2.72 +    lthy |> (Data.map o map_index) (fn (i, {naming, operations, after_close, brittle, target}) =>
    2.73 +      make_lthy (naming, operations, after_close, brittle,
    2.74          target
    2.75          |> Context_Position.set_visible false
    2.76          |> f (n - i - 1)
    2.77 @@ -153,10 +154,14 @@
    2.78  
    2.79  (* brittle context -- implicit for nested structures *)
    2.80  
    2.81 -val mark_brittle = Data.map (fn ([data], _) => ([data], true) | x => x);
    2.82 +fun mark_brittle lthy =
    2.83 +  if level lthy = 1
    2.84 +  then map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
    2.85 +    (naming, operations, after_close, true, target)) lthy
    2.86 +  else lthy;
    2.87  
    2.88  fun assert_nonbrittle lthy =
    2.89 -  if snd (Data.get lthy) orelse level lthy > 1
    2.90 +  if #brittle (get_first_lthy lthy)
    2.91    then error "Brittle local theory context"
    2.92    else lthy;
    2.93  
    2.94 @@ -167,8 +172,8 @@
    2.95  val full_name = Name_Space.full_name o naming_of;
    2.96  
    2.97  fun map_naming f =
    2.98 -  map_first_lthy (fn (naming, operations, after_close, target) =>
    2.99 -    (f naming, operations, after_close, target));
   2.100 +  map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
   2.101 +    (f naming, operations, after_close, brittle, target));
   2.102  
   2.103  val conceal = map_naming Name_Space.conceal;
   2.104  val new_group = map_naming Name_Space.new_group;
   2.105 @@ -302,8 +307,8 @@
   2.106  (* init *)
   2.107  
   2.108  fun init naming operations target =
   2.109 -  target |> (Data.map o apfst)
   2.110 -    (fn [] => [make_lthy (naming, operations, I, target)]
   2.111 +  target |> Data.map
   2.112 +    (fn [] => [make_lthy (naming, operations, I, false, target)]
   2.113        | _ => error "Local theory already initialized")
   2.114    |> checkpoint;
   2.115  
     3.1 --- a/src/Pure/Isar/toplevel.ML	Wed May 22 19:44:51 2013 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Wed May 22 22:56:17 2013 +0200
     3.3 @@ -110,14 +110,14 @@
     3.4  (* local theory wrappers *)
     3.5  
     3.6  val loc_init = Named_Target.context_cmd;
     3.7 -val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.assert_nonbrittle #> Local_Theory.exit_global;
     3.8 +val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
     3.9  
    3.10  fun loc_begin loc (Context.Theory thy) =
    3.11        (Context.Theory o loc_exit, loc_init (the_default ("-", Position.none) loc) thy)
    3.12    | loc_begin NONE (Context.Proof lthy) =
    3.13        (Context.Proof o Local_Theory.restore, lthy)
    3.14    | loc_begin (SOME loc) (Context.Proof lthy) =
    3.15 -      (Context.Proof o Named_Target.reinit lthy, loc_init loc (loc_exit lthy));
    3.16 +      (Context.Proof o Named_Target.reinit lthy, loc_init loc (loc_exit (Local_Theory.assert_nonbrittle lthy)));
    3.17  
    3.18  
    3.19  (* datatype node *)