Fixed a bug causing inconsistent states during proof editting.

Some toplevel commands (for instance the experimental bullets) are
composed of several atomic commands, the failure of one must imply
the failure of the whole toplevel command. This commit introduces
a system of transaction to that effect.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14087 85f007b7-540e-0410-9357-904b9bb8a0f7

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