Déplacement de save_thm and co de PFedit vers Command

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

2 files changed, 22 insertions, 57 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d033ac5d2e..fa69b6e73e 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -28,7 +28,8 @@ type proof_topstate = {
   top_goal : goal;
   top_strength : strength }
 
-let proof_edits = (Edit.empty() : (string,pftreestate,proof_topstate) Edit.t)
+let proof_edits =
+  (Edit.empty() : (identifier,pftreestate,proof_topstate) Edit.t)
 
 let get_all_proof_names () = Edit.dom proof_edits
 
@@ -36,8 +37,7 @@ let msg_proofs use_resume =
   match Edit.dom proof_edits with
     | [] -> [< 'sPC ; 'sTR"(No proof-editing in progress)." >]
     | l ->  [< 'sTR"." ; 'fNL ; 'sTR"Proofs currently edited:" ; 'sPC ;
-               (prlist_with_sep pr_spc pr_str (get_all_proof_names ())) ;
-	       'sTR"." ;
+               (print_idl (get_all_proof_names ())) ; 'sTR"." ;
                (if use_resume then [< 'fNL ; 'sTR"Use \"Resume\" first." >]
               	else [< >])
             >]
@@ -178,46 +178,19 @@ let undo n =
     errorlabstrm "Pfedit.undo" [< 'sTR"No focused proof"; msg_proofs true >]
 
 (*********************************************************************)
-(*              Saving  functions                                    *)
+(*                Proof releasing                                    *)
 (*********************************************************************)
 
-let save_named opacity =
+let release_proof () =
   let (pfs,ts) = get_state() 
   and ident = get_current_proof_name () in
   let {evar_concl=concl} = ts.top_goal 
   and strength = ts.top_strength in
-  let pfterm = extract_pftreestate pfs in 
-  declare_constant (id_of_string ident)
-    ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl }, 
-     strength);
+  let pfterm = extract_pftreestate pfs in
   del_proof ident;
-  if Options.is_verbose() then message (ident ^ " is defined")
-    
-let save_anonymous opacity save_ident strength =
-  let (pfs,ts) = get_state() 
-  and ident = get_current_proof_name() in
-  let {evar_concl=concl} = ts.top_goal in
-  (* we do not consider default ts.top_strength *)
-  let pfterm = extract_pftreestate pfs in 
-  if ident = "Unnamed_thm" then
-    declare_constant (id_of_string save_ident)
-      ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl }, 
-       strength)
-  else begin
-    message("Overriding name " ^ ident ^ " and using " ^ save_ident);
-    declare_constant (id_of_string save_ident)
-      ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl }, 
-       strength)
-  end;
-  del_proof ident;
-  if Options.is_verbose() then message (save_ident ^ " is defined")
-    
-let save_anonymous_thm opacity id =
-  save_anonymous opacity id NeverDischarge
-
-let save_anonymous_remark opacity id =
-  let path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in
-  save_anonymous opacity id (make_strength path)
+  (ident,
+   ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl },
+    strength))
 
 (*********************************************************************)
 (*              Abort   functions                                    *)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7f6747721e..0bf91510b6 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -32,7 +32,7 @@ val check_no_pending_proofs : unit -> unit
 (*s [abort_proof name] aborts proof of name [name] or failed if no proof
 has this name *)
 
-val abort_proof : string -> unit
+val abort_proof : identifier -> unit
 
 (* [abort_current_proof ()] aborts current focused proof or failed if
     no proof is focused *)
@@ -60,7 +60,7 @@ val reset_undo : unit -> unit
 
 (*s [start_proof s str env t] starts a proof of name [s] and conclusion [t] *)
 
-val start_proof : string -> strength -> env -> constr -> unit
+val start_proof : identifier -> strength -> env -> constr -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
@@ -75,13 +75,21 @@ val resume_last_proof : unit -> unit
 (* [resume_proof name] focuses on the proof of name [name] or
    raises [UserError] if no proof has name [name] *)
 
-val resume_proof : string -> unit
+val resume_proof : identifier -> unit
 
 (* [suspend_proof ()] unfocuses the current focused proof or
    failed with [UserError] if no proof is currently focused *)
 
 val suspend_proof : unit -> unit
 
+(*s [release_proof ()] turns the current proof into a constant with
+    its name and strength, then remove the proof from the set of
+    pending proofs; it fails if there is no current proof of if it is
+    not completed *)
+
+val release_proof : unit ->
+  identifier * (Declarations.constant_entry * strength)
+
 (*s [get_pftreestate ()] returns the current focused pending proof or
    raises [UserError "no focused proof"] *)
 
@@ -100,11 +108,11 @@ val get_current_goal_context : unit -> evar_declarations * env
 (*s [get_current_proof_name ()] return the name of the current focused
     proof or failed if no proof is focused *)
 
-val get_current_proof_name : unit -> string
+val get_current_proof_name : unit -> identifier
 
 (* [get_all_proof_names ()] returns the list of all pending proof names *)
 
-val get_all_proof_names : unit -> string list
+val get_all_proof_names : unit -> identifier list
 
 (*s [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
    current focused proof or raises a UserError if no proof is focused or
@@ -125,22 +133,6 @@ val by : tactic -> unit
 
 val instantiate_nth_evar_com : int -> Coqast.t -> unit
 
-(*s [save_named b] saves the current completed proof under the name it
-was started; boolean [b] tells if the theorem is declared opaque; it
-fails if the proof is not completed *)
-
-val save_named : bool -> 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 *)
-
-val save_anonymous_thm : 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
-
 (*s To deal with subgoal focus *)
 
 val make_focus : int -> unit