implicit name space grouping for theory/local_theory transactions;
authorwenzelm
Tue Nov 17 14:51:32 2009 +0100 (2009-11-17 ago)
changeset 33725a8481da77270
parent 33724 5ee13e0428d2
child 33726 0878aecbf119
implicit name space grouping for theory/local_theory transactions;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Nov 17 14:50:55 2009 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Nov 17 14:51:32 2009 +0100
     1.3 @@ -419,7 +419,13 @@
     1.4      | _ => raise UNDEF));
     1.5  
     1.6  fun theory' f = transaction (fn int =>
     1.7 -  (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (f int thy), NONE)
     1.8 +  (fn Theory (Context.Theory thy, _) =>
     1.9 +      let val thy' = thy
    1.10 +        |> Sign.new_group
    1.11 +        |> Theory.checkpoint
    1.12 +        |> f int
    1.13 +        |> Sign.reset_group;
    1.14 +      in Theory (Context.Theory thy', NONE) end
    1.15      | _ => raise UNDEF));
    1.16  
    1.17  fun theory f = theory' (K f);
    1.18 @@ -442,7 +448,10 @@
    1.19    (fn Theory (gthy, _) =>
    1.20          let
    1.21            val finish = loc_finish loc gthy;
    1.22 -          val lthy' = f int (loc_begin loc gthy);
    1.23 +          val lthy' = loc_begin loc gthy
    1.24 +            |> Local_Theory.new_group
    1.25 +            |> f int
    1.26 +            |> Local_Theory.reset_group;
    1.27          in Theory (finish lthy', SOME lthy') end
    1.28      | _ => raise UNDEF));
    1.29  
    1.30 @@ -491,14 +500,14 @@
    1.31  in
    1.32  
    1.33  fun local_theory_to_proof' loc f = begin_proof
    1.34 -  (fn int => fn gthy => f int (loc_begin loc gthy))
    1.35 -  (loc_finish loc);
    1.36 +  (fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy)))
    1.37 +  (fn gthy => loc_finish loc gthy o Local_Theory.reset_group);
    1.38  
    1.39  fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
    1.40  
    1.41  fun theory_to_proof f = begin_proof
    1.42 -  (K (fn Context.Theory thy => f thy | _ => raise UNDEF))
    1.43 -  (K (Context.Theory o ProofContext.theory_of));
    1.44 +  (K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
    1.45 +  (K (Context.Theory o Sign.reset_group o ProofContext.theory_of));
    1.46  
    1.47  end;
    1.48  
    1.49 @@ -531,7 +540,7 @@
    1.50  
    1.51  fun skip_proof_to_theory pred = transaction (fn _ =>
    1.52    (fn SkipProof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
    1.53 -  | _ => raise UNDEF));
    1.54 +    | _ => raise UNDEF));
    1.55  
    1.56  
    1.57