From d10841e20af67563b60d7cf91e251079b35b6636 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 29 Apr 2011 15:03:25 +0000
Subject: 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
---
 plugins/decl_mode/g_decl_mode.ml4 | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index aa187cc749..5ac3e8e9ed 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. *)
-- 
cgit v1.2.3