diff options
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 16 | ||||
| -rw-r--r-- | proofs/proof.ml | 53 | ||||
| -rw-r--r-- | proofs/proof.mli | 12 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 16 |
4 files changed, 78 insertions, 19 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index aa187cc74..5ac3e8e9e 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -67,7 +67,7 @@ let vernac_decl_proof () = if Proof.is_done pf then Util.error "Nothing left to prove here." else - begin + Proof.transaction pf begin fun () -> Decl_proof_instr.go_to_proof_mode () ; Proof_global.set_proof_mode "Declarative" ; Vernacentries.print_subgoals () @@ -75,13 +75,17 @@ let vernac_decl_proof () = (* spiwack: some bureaucracy is not performed here *) let vernac_return () = - Decl_proof_instr.return_from_tactic_mode () ; - Proof_global.set_proof_mode "Declarative" ; - Vernacentries.print_subgoals () + Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + Decl_proof_instr.return_from_tactic_mode () ; + Proof_global.set_proof_mode "Declarative" ; + Vernacentries.print_subgoals () + end let vernac_proof_instr instr = - Decl_proof_instr.proof_instr instr; - Vernacentries.print_subgoals () + Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + Decl_proof_instr.proof_instr instr; + Vernacentries.print_subgoals () + end (* We create a new parser entry [proof_mode]. The Declarative proof mode will replace the normal parser entry for tactics with this one. *) diff --git a/proofs/proof.ml b/proofs/proof.ml index b932e95f9..3feef112f 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -92,6 +92,8 @@ type proof = { (* current proof_state *) mutable state : proof_state; (* The undo stack *) mutable undo_stack : undo_action list; + (* secondary undo stacks used for transactions *) + mutable transactions : undo_action list list; info : proof_info } @@ -103,6 +105,7 @@ let start goals = focus_stack = [] ; intel = Store.empty} ; undo_stack = [] ; + transactions = [] ; info = { endline_tactic = Proofview.tclUNIT (); initial_conclusions = List.map snd goals } } @@ -161,14 +164,17 @@ let pop_focus pr = raise FullyUnfocused (* Auxiliary function to push a [proof_state] onto the undo stack. *) -let push_undo save ({ undo_stack = stack } as pr) = - pr.undo_stack <- save::stack +let push_undo save pr = + match pr.transactions with + | [] -> pr.undo_stack <- save::pr.undo_stack + | stack::trans' -> pr.transactions <- (save::stack)::trans' (* Auxiliary function to pop and read a [save_state] from the undo stack. *) exception EmptyUndoStack -let pop_undo pr = - match pr.undo_stack with - | state::stack -> pr.undo_stack <- stack; state +let pop_undo pr = + match pr.transactions , pr.undo_stack with + | [] , state::stack -> pr.undo_stack <- stack; state + | (state::stack)::trans', _ -> pr.transactions <- stack::trans'; state | _ -> raise EmptyUndoStack @@ -286,7 +292,42 @@ let run_tactic env tac pr = with e -> restore_state starting_point pr; raise e - + + +(*** Transactions ***) + +let init_transaction pr = + pr.transactions <- []::pr.transactions + +let commit_stack pr stack = + let push s = push_undo s pr in + List.iter push (List.rev stack) + +(* Invariant: [commit] should be called only when a transaction + is open. It closes the current transaction. *) +let commit pr = + match pr.transactions with + | stack::trans' -> + pr.transactions <- trans'; + commit_stack pr stack + | [] -> assert false + +(* Invariant: [rollback] should be called only when a transaction + is open. It closes the current transaction. *) +let rec rollback pr = + try + undo pr; + rollback pr + with EmptyUndoStack -> + match pr.transactions with + | []::trans' -> pr.transactions <- trans' + | _ -> assert false + + +let transaction pr t = + init_transaction pr; + try t (); commit pr + with e -> rollback pr; raise e (*** Compatibility layer with <=v8.2 ***) diff --git a/proofs/proof.mli b/proofs/proof.mli index eed0bc481..cbde9244a 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -129,6 +129,18 @@ val with_end_tac : proof -> unit Proofview.tactic -> unit Proofview.tactic val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> unit +(*** Transactions ***) + +(* A transaction chains several commands into a single one. For instance, + a focusing command and a tactic. Transactions are such that if + any of the atomic action fails, the whole transaction fails. + + During a transaction, the undo visible undo stack is constituted only + of the actions performed done during the transaction. + + [transaction p f] can be called on an [f] using, itself, [transaction p].*) +val transaction : proof -> (unit -> unit) -> unit + (*** Compatibility layer with <=v8.2 ***) module V82 : sig val subgoals : proof -> Goal.goal list Evd.sigma diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 088fb3b96..a9e390538 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -687,13 +687,15 @@ let vernac_solve n bullet tcom b = if not (refining ()) then error "Unknown command of the non proof-editing mode."; let p = Proof_global.give_me_the_proof () in - Option.iter (put_bullet p) bullet ; - solve_nth n (Tacinterp.hide_interp tcom None) ~with_end_tac:b; - (* in case a strict subtree was completed, - go back to the top of the prooftree *) - Proof_global.maximal_unfocus command_focus p; - print_subgoals(); - if !pcoq <> None then (Option.get !pcoq).solve n + Proof.transaction p begin fun () -> + Option.iter (put_bullet p) bullet ; + solve_nth n (Tacinterp.hide_interp tcom None) ~with_end_tac:b; + (* in case a strict subtree was completed, + go back to the top of the prooftree *) + Proof_global.maximal_unfocus command_focus p; + print_subgoals(); + if !pcoq <> None then (Option.get !pcoq).solve n + end (* A command which should be a tactic. It has been |