Uniformisation des 'Save def_tok id'

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

3 files changed, 32 insertions, 58 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index c7fcc0f3b1..e8bc17cc34 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -461,23 +461,19 @@ let save_named opacity =
   let id,(const,strength) = Pfedit.cook_proof () in
   save opacity id const strength
 
-let save_anonymous_with_strength opacity save_ident id const strength =
+let check_anonymity id save_ident =
   if atompart_of_id id <> "Unnamed_thm" then
-    message("Overriding name "^(string_of_id id)^" and using "^save_ident);
-  save opacity (id_of_string save_ident) const strength
+    message("Overriding name "^(string_of_id id)^" and using "^save_ident)
 
 let save_anonymous opacity save_ident =
   let id,(const,strength) = Pfedit.cook_proof () in
-  save_anonymous_with_strength opacity save_ident id const strength
+  check_anonymity id save_ident;
+  save opacity (id_of_string save_ident) const strength
 
-let save_anonymous_thm opacity save_ident =
+let save_anonymous_with_strength strength opacity save_ident =
   let id,(const,_) = Pfedit.cook_proof () in
-  save_anonymous_with_strength opacity save_ident id const NeverDischarge
-
-let save_anonymous_remark opacity save_ident =
-  let id,(const,_) = Pfedit.cook_proof ()
-  and path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in
-  save_anonymous_with_strength opacity save_ident id const (make_strength path)
+  check_anonymity id save_ident;
+  save opacity (id_of_string save_ident) const strength
 
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 83ce53567a..b7b9d0f130 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -63,14 +63,14 @@ under the name [name] and respects the strength of the declaration *)
 
 val save_anonymous : bool -> string -> unit
 
-(* [save_anonymous_thm b name] behaves as [save_named] but declares the
-theorem under the name [name] and gives it the strength of a theorem *)
+(* [save_anonymous_with_strength s b name] behaves as [save_anonymous] but
+   declares the theorem under the name [name] and gives it the
+   strength [strength] *)
 
-val save_anonymous_thm : bool -> string -> unit
+val save_anonymous_with_strength : strength -> bool -> string -> unit
 
-(* [save_anonymous_remark b name] behaves as [save_named] but declares the
-theorem under the name [name] and gives it the strength of a remark *)
-
-val save_anonymous_remark : bool -> string -> unit
+(* [get_current_context ()] returns the evar context and env of the
+   current open proof if any, otherwise returns the empty evar context
+   and the current global env *)
 
 val get_current_context : unit -> Proof_type.enamed_declarations * Environ.env
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d56b566025..712e9ff7ae 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -577,6 +577,17 @@ let _ =
 	      Impargs.declare_implicits (locate_qualid dummy_loc qid))
        | _  -> bad_vernac_args "IMPLICITS")
 
+let interp_definition_kind = function
+  | "THEOREM" -> (NeverDischarge,     true)
+  | "LEMMA"   -> (NeverDischarge,     true)
+  | "FACT"    -> (make_strength_1 (), true)
+  | "REMARK"  -> (make_strength_0 (), true)
+  | "DEFINITION" -> (NeverDischarge,     false)
+  | "LET"        -> (make_strength_1 (), false)
+  | "LETTOP"     -> (NeverDischarge,     false)
+  | "LOCAL"      -> (make_strength_0 (), false)
+  | _       -> anomaly "Unexpected definition kind"
+
 let _ =
   add "SaveNamed"
     (function 
@@ -603,29 +614,16 @@ let _ =
 let _ =
   add "SaveAnonymous"
     (function 
-       | [VARG_IDENTIFIER id] -> 
-	   (fun () -> 
-	      if_verbose show_script ();
-              save_anonymous true (string_of_id id))
-       | _ -> bad_vernac_args "SaveAnonymous")
-
-let _ =
-  add "SaveAnonymousThm"
-    (function 
-       | [VARG_IDENTIFIER id] -> 
+       | [VARG_STRING kind; VARG_IDENTIFIER id] -> 
 	   (fun () -> 
+	      let (strength, opacity) = interp_definition_kind kind in
 	      if_verbose show_script ();
-              save_anonymous_thm true (string_of_id id))
-       | _ -> bad_vernac_args "SaveAnonymousThm")
-
-let _ =
-  add "SaveAnonymousRmk"
-    (function 
+              save_anonymous_with_strength strength opacity (string_of_id id))
        | [VARG_IDENTIFIER id] -> 
 	   (fun () -> 
 	      if_verbose show_script ();
-              save_anonymous_remark true (string_of_id id))
-       | _ -> bad_vernac_args "SaveAnonymousRmk")
+              save_anonymous true (string_of_id id))
+       | _ -> bad_vernac_args "SaveAnonymous")
 
 let _ =
   add "TRANSPARENT"
@@ -853,17 +851,7 @@ let _ =
   add "StartProof"
     (function 
        | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR com] ->
-	   let stre = match kind with
-	     | "THEOREM" -> NeverDischarge
-             | "LEMMA" -> NeverDischarge
-             | "FACT" -> make_strength_1 ()
-             | "REMARK" -> make_strength_0 ()
-             | "DEFINITION" -> NeverDischarge
-             | "LET" -> make_strength_2 ()
-	     | "LETTOP" -> NotDeclare
-             | "LOCAL" -> make_strength_0 ()
-             | _       -> anomaly "Unexpected string"
-           in 
+	   let stre = fst (interp_definition_kind kind) in
 	   fun () ->
              begin
                if (kind = "LETTOP") && not(refining ()) then
@@ -885,17 +873,7 @@ let _ =
 			    | _ -> bad_vernac_args "")
 			 coml 
 	   in
-	   let (stre,opacity) = match kind with
-	     | "THEOREM" -> (NeverDischarge,true)
-             | "LEMMA" -> (NeverDischarge,true)
-             | "FACT" -> (make_strength_1(),true)
-             | "REMARK" -> (make_strength_0(),true)
-             | "DEFINITION" -> (NeverDischarge,false)
-             | "LET" -> (make_strength_1(),false)
-	     | "LETTOP" -> (NeverDischarge,false)
-             | "LOCAL" -> (make_strength_0(),false)
-             | _       -> anomaly "Unexpected string" 
-	   in
+	   let (stre,opacity) = interp_definition_kind kind in
            (fun () ->
               try
             	States.with_heavy_rollback