src/Pure/Isar/toplevel.ML
changeset 49012 8686c36fa27d
parent 49011 9c68e43502ce
child 49042 01041f7bf9b4
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Aug 30 19:18:49 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Aug 30 21:23:04 2012 +0200
     1.3 @@ -53,9 +53,10 @@
     1.4    val ignored: Position.T -> transition
     1.5    val malformed: Position.T -> string -> transition
     1.6    val is_malformed: transition -> bool
     1.7 -  val theory: (theory -> theory) -> transition -> transition
     1.8 +  val join_recent_proofs: state -> unit
     1.9    val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
    1.10    val theory': (bool -> theory -> theory) -> transition -> transition
    1.11 +  val theory: (theory -> theory) -> transition -> transition
    1.12    val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
    1.13    val end_local_theory: transition -> transition
    1.14    val open_target: (generic_theory -> local_theory) -> transition -> transition
    1.15 @@ -422,15 +423,21 @@
    1.16  val unknown_context = imperative (fn () => warning "Unknown context");
    1.17  
    1.18  
    1.19 -(* theory transitions *)
    1.20 +(* forked proofs *)
    1.21 +
    1.22 +val begin_proofs_thy = Context.theory_map Thm.begin_proofs #> Theory.checkpoint;
    1.23 +val begin_proofs = Context.mapping begin_proofs_thy (Local_Theory.raw_theory begin_proofs_thy);
    1.24  
    1.25 -val global_theory_group =
    1.26 -  Sign.new_group #>
    1.27 -  Context.theory_map Thm.begin_proofs #> Theory.checkpoint;
    1.28 +fun join_recent_proofs st =
    1.29 +  (case try proof_of st of
    1.30 +    SOME prf => Proof.join_recent_proofs prf
    1.31 +  | NONE =>
    1.32 +      (case try theory_of st of
    1.33 +        SOME thy => Thm.join_recent_proofs thy
    1.34 +      | NONE => ()));
    1.35  
    1.36 -val local_theory_group =
    1.37 -  Local_Theory.new_group #>
    1.38 -  Local_Theory.raw_theory (Context.theory_map Thm.begin_proofs #> Theory.checkpoint);
    1.39 +
    1.40 +(* theory transitions *)
    1.41  
    1.42  fun generic_theory f = transaction (fn _ =>
    1.43    (fn Theory (gthy, _) => Theory (f gthy, NONE)
    1.44 @@ -439,7 +446,8 @@
    1.45  fun theory' f = transaction (fn int =>
    1.46    (fn Theory (Context.Theory thy, _) =>
    1.47        let val thy' = thy
    1.48 -        |> global_theory_group
    1.49 +        |> Sign.new_group
    1.50 +        |> Theory.checkpoint
    1.51          |> f int
    1.52          |> Sign.reset_group;
    1.53        in Theory (Context.Theory thy', NONE) end
    1.54 @@ -478,9 +486,11 @@
    1.55  fun local_theory_presentation loc f = present_transaction (fn int =>
    1.56    (fn Theory (gthy, _) =>
    1.57          let
    1.58 -          val (finish, lthy) = loc_begin loc gthy;
    1.59 +          val (finish, lthy) = gthy
    1.60 +            |> begin_proofs
    1.61 +            |> loc_begin loc;
    1.62            val lthy' = lthy
    1.63 -            |> local_theory_group
    1.64 +            |> Local_Theory.new_group
    1.65              |> f int
    1.66              |> Local_Theory.reset_group;
    1.67          in Theory (finish lthy', SOME lthy') end
    1.68 @@ -534,15 +544,19 @@
    1.69  
    1.70  fun local_theory_to_proof' loc f = begin_proof
    1.71    (fn int => fn gthy =>
    1.72 -    let val (finish, lthy) = loc_begin loc gthy
    1.73 -    in (finish o Local_Theory.reset_group, f int (local_theory_group lthy)) end);
    1.74 +    let val (finish, lthy) = gthy
    1.75 +      |> begin_proofs
    1.76 +      |> loc_begin loc;
    1.77 +    in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
    1.78  
    1.79  fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
    1.80  
    1.81  fun theory_to_proof f = begin_proof
    1.82    (fn _ => fn gthy =>
    1.83      (Context.Theory o Sign.reset_group o Proof_Context.theory_of,
    1.84 -      (case gthy of Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF)));
    1.85 +      (case begin_proofs gthy of
    1.86 +        Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy))
    1.87 +      | _ => raise UNDEF)));
    1.88  
    1.89  end;
    1.90  
    1.91 @@ -552,12 +566,12 @@
    1.92      | _ => raise UNDEF));
    1.93  
    1.94  val present_proof = present_transaction (fn _ =>
    1.95 -  (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
    1.96 +  (fn Proof (prf, x) => Proof (Proof_Node.apply Proof.begin_proofs prf, x)
    1.97      | skip as SkipProof _ => skip
    1.98      | _ => raise UNDEF));
    1.99  
   1.100  fun proofs' f = transaction (fn int =>
   1.101 -  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
   1.102 +  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int o Proof.begin_proofs) prf, x)
   1.103      | skip as SkipProof _ => skip
   1.104      | _ => raise UNDEF));
   1.105