Modification afin de permettre plusieurs modifs successives d'une commande

vernac (ici la commande Save)


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

1 files changed, 31 insertions, 5 deletions

diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 4918910d35..a4b62c53c4 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -248,6 +248,7 @@ let register id n =
   let id' = match n with None -> id | Some id' -> id' in
   Penv.register id id'
 
+(*
 let wrap_save_named b =
   let pf_id = Pfedit.get_current_proof_name () in
   Command.save_named b;
@@ -257,12 +258,37 @@ let wrap_save_anonymous b id =
   let pf_id = Pfedit.get_current_proof_name () in
   Command.save_anonymous b (string_of_id id);
   register pf_id (Some id)
-
-let _ = add "SaveNamed"
-    (function [] -> (fun () -> if_verbose show_script ();
-		              wrap_save_named true)
+*)
+
+let _ = 
+  let current_save = Vernacinterp.vinterp_map "SaveNamed" in
+    add "SaveNamed"
+      (function [] -> (fun () -> let pf_id =  Pfedit.get_current_proof_name () in
+			 current_save [] ();
+			 register pf_id None)
+	 |   _  -> assert false)
+
+let _ = 
+  let current_defined = Vernacinterp.vinterp_map "DefinedNamed" in
+    add "DefinedNamed"
+      (function [] -> (fun () -> let pf_id = Pfedit.get_current_proof_name () in
+			 current_defined [] ();
+			 register pf_id None)
+	 | _ -> assert false)
+
+let _ =
+  let current_saveanonymous = Vernacinterp.vinterp_map "SaveAnonymous" in
+    add "SaveAnonymous"
+      (function [VARG_IDENTIFIER id] -> 
+	 (fun () -> let pf_id = Pfedit.get_current_proof_name () in
+	    current_saveanonymous [VARG_IDENTIFIER id] ();
+	    register pf_id (Some id))
     |   _  -> assert false)
 
+(* Old version that does not allow multiple modifications of the "Save" command *)
+(*
+let _ = 
+
 let _ = add "DefinedNamed"
     (function [] -> (fun () -> if_verbose show_script ();
 		              wrap_save_named false)
@@ -273,4 +299,4 @@ let _ = add "SaveAnonymous"
        (fun () -> if_verbose show_script ();
 	          wrap_save_anonymous true id)
     |   _  -> assert false)
-
+*)