transactions now always see quasi-functional intermediate checkpoint;
authorwenzelm
Fri Jan 06 15:18:21 2006 +0100 (2006-01-06)
changeset 18592451d622bb4a9
parent 18591 04b9f2bf5a48
child 18593 4ce4dba4af07
transactions now always see quasi-functional intermediate checkpoint;
removed obsolete theory_theory_to_proof;
added
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Jan 06 15:18:20 2006 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Jan 06 15:18:21 2006 +0100
     1.3 @@ -74,7 +74,6 @@
     1.4    val theory': (bool -> theory -> theory) -> transition -> transition
     1.5    val theory_context: (theory -> theory * Proof.context) -> transition -> transition
     1.6    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
     1.7 -  val theory_theory_to_proof: (theory -> Proof.state) -> transition -> transition
     1.8    val proof: (Proof.state -> Proof.state) -> transition -> transition
     1.9    val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
    1.10    val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
    1.11 @@ -253,11 +252,11 @@
    1.12  
    1.13  val stale_theory = ERROR_MESSAGE "Stale theory encountered after succesful execution!";
    1.14  
    1.15 -fun checkpoint_node true (Theory (thy, ctxt)) = Theory (Theory.checkpoint thy, ctxt)
    1.16 -  | checkpoint_node _ node = node;
    1.17 +fun checkpoint_node (Theory (thy, ctxt)) = Theory (Theory.checkpoint thy, ctxt)
    1.18 +  | checkpoint_node node = node;
    1.19  
    1.20 -fun copy_node true (Theory (thy, ctxt)) = Theory (Theory.copy thy, ctxt)
    1.21 -  | copy_node _ node = node;
    1.22 +fun copy_node (Theory (thy, ctxt)) = Theory (Theory.copy thy, ctxt)
    1.23 +  | copy_node node = node;
    1.24  
    1.25  fun return (result, NONE) = result
    1.26    | return (result, SOME exn) = raise FAILURE (result, exn);
    1.27 @@ -274,12 +273,11 @@
    1.28  
    1.29  in
    1.30  
    1.31 -fun transaction _ _ _ (State NONE) = raise UNDEF
    1.32 -  | transaction save hist f (State (SOME (node, term))) =
    1.33 +fun transaction _ _ (State NONE) = raise UNDEF
    1.34 +  | transaction hist f (State (SOME (node, term))) =
    1.35        let
    1.36 -        val save = true;  (* FIXME *)
    1.37 -        val cont_node = History.map (checkpoint_node save) node;
    1.38 -        val back_node = History.map (copy_node save) cont_node;
    1.39 +        val cont_node = History.map checkpoint_node node;
    1.40 +        val back_node = History.map copy_node cont_node;
    1.41          fun state nd = State (SOME (nd, term));
    1.42          fun normal_state nd = (state nd, NONE);
    1.43          fun error_state nd exn = (state nd, SOME exn);
    1.44 @@ -287,7 +285,7 @@
    1.45          val (result, err) =
    1.46            cont_node
    1.47            |> (f
    1.48 -              |> (if hist then History.apply_copy (copy_node save) else History.map)
    1.49 +              |> (if hist then History.apply_copy copy_node else History.map)
    1.50                |> debug_trans
    1.51                |> interruptible
    1.52                |> transform_error)
    1.53 @@ -303,8 +301,8 @@
    1.54    | mapping _ state = state;
    1.55  
    1.56  val no_body_context = mapping (fn Theory (thy, _) => Theory (thy, NONE) | node => node);
    1.57 -val checkpoint = mapping (checkpoint_node true);
    1.58 -val copy = mapping (copy_node true);
    1.59 +val checkpoint = mapping checkpoint_node;
    1.60 +val copy = mapping copy_node;
    1.61  
    1.62  end;
    1.63  
    1.64 @@ -324,7 +322,7 @@
    1.65    Kill |                                                (*abort node*)
    1.66    Keep of bool -> state -> unit |                       (*peek at state*)
    1.67    History of node History.T -> node History.T |         (*history operation (undo etc.)*)
    1.68 -  Transaction of bool * bool * (bool -> node -> node);  (*node transaction*)
    1.69 +  Transaction of bool * (bool -> node -> node);         (*node transaction*)
    1.70  
    1.71  fun undo_limit int = if int then NONE else SOME 0;
    1.72  
    1.73 @@ -343,8 +341,7 @@
    1.74    | apply_tr int (Keep f) state = (raise_interrupt (f int) state; state)
    1.75    | apply_tr _ (History _) (State NONE) = raise UNDEF
    1.76    | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term))
    1.77 -  | apply_tr int (Transaction (save, hist, f)) state =
    1.78 -      transaction (int orelse save) hist (fn x => f int x) state;
    1.79 +  | apply_tr int (Transaction (hist, f)) state = transaction hist (fn x => f int x) state;
    1.80  
    1.81  fun apply_union _ [] state = raise FAILURE (state, UNDEF)
    1.82    | apply_union int (tr :: trs) state =
    1.83 @@ -434,8 +431,8 @@
    1.84  val kill = add_trans Kill;
    1.85  val keep' = add_trans o Keep;
    1.86  val history = add_trans o History;
    1.87 -fun map_current f = add_trans (Transaction (false, false, f));
    1.88 -fun app_current save f = add_trans (Transaction (save, true, f));
    1.89 +fun map_current f = add_trans (Transaction (false, f));
    1.90 +fun app_current f = add_trans (Transaction (true, f));
    1.91  
    1.92  fun keep f = add_trans (Keep (fn _ => f));
    1.93  fun imperative f = keep (fn _ => f ());
    1.94 @@ -448,28 +445,21 @@
    1.95  
    1.96  (* typed transitions *)
    1.97  
    1.98 -fun theory f = app_current false
    1.99 +fun theory f = app_current
   1.100    (K (fn Theory (thy, _) => Theory (f thy, NONE) | _ => raise UNDEF));
   1.101  
   1.102 -fun theory' f = app_current false (fn int =>
   1.103 +fun theory' f = app_current (fn int =>
   1.104    (fn Theory (thy, _) => Theory (f int thy, NONE) | _ => raise UNDEF));
   1.105  
   1.106 -fun theory_context f = app_current false
   1.107 +fun theory_context f = app_current
   1.108    (K (fn Theory (thy, _) => Theory (apsnd SOME (f thy)) | _ => raise UNDEF));
   1.109  
   1.110 -fun to_proof save f = app_current save (fn int =>
   1.111 +fun theory_to_proof f = app_current (fn int =>
   1.112    (fn Theory (thy, _) =>
   1.113 -      let val st = f thy in
   1.114 -        if save orelse Theory.eq_thy (thy, Proof.theory_of st) then ()
   1.115 -        else error "Theory changed at start of proof";
   1.116 -        if ! skip_proofs then
   1.117 -          SkipProof ((History.init (undo_limit int) 0, #1 (Proof.global_skip_proof int st)), thy)
   1.118 -        else Proof (ProofHistory.init (undo_limit int) st, thy)
   1.119 -      end
   1.120 -    | _ => raise UNDEF));
   1.121 -
   1.122 -val theory_to_proof = to_proof false;
   1.123 -val theory_theory_to_proof = to_proof true;
   1.124 +    if ! skip_proofs then
   1.125 +      SkipProof ((History.init (undo_limit int) 0, #1 (Proof.global_skip_proof int (f thy))), thy)
   1.126 +    else Proof (ProofHistory.init (undo_limit int) (f thy), thy)
   1.127 +  | _ => raise UNDEF));
   1.128  
   1.129  fun proofs' f = map_current (fn int =>
   1.130    (fn Proof (prf, orig_thy) => Proof (ProofHistory.applys (f int) prf, orig_thy)