author wenzelm Tue Nov 17 14:51:32 2009 +0100 (2009-11-17 ago) changeset 33725 a8481da77270 parent 33724 5ee13e0428d2 child 33726 0878aecbf119
implicit name space grouping for theory/local_theory transactions;
```     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
```