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

7 files changed, 94 insertions, 84 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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8803933e94..feb4bf69a6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -98,7 +98,7 @@ let mutual_fix   = Tacmach.mutual_fix
 let fix f n      = mutual_fix [f] [n] []
 
 let fix_noname n =  
-  let id = id_of_string (Pfedit.get_current_proof_name ()) in
+  let id = Pfedit.get_current_proof_name () in
   fix id n
 
 let dyn_mutual_fix argsl gl = 
@@ -120,7 +120,7 @@ let mutual_cofix = Tacmach.mutual_cofix
 let cofix f      =  mutual_cofix [f] []
 
 let cofix_noname n =  
-  let id = id_of_string (Pfedit.get_current_proof_name ()) in
+  let id = Pfedit.get_current_proof_name () in
   cofix id n
 
 let dyn_mutual_cofix argsl gl = 
@@ -1634,27 +1634,31 @@ let abstract_subproof name tac gls =
   in
   let na = next_global_ident_away name
              (ids_of_sign global_sign)  in 
-  let nas = string_of_id na in
   let concl = Sign.it_sign (fun t id typ -> mkNamedProd id typ t)
                 (pf_concl gls) sign in
   let env' = change_hyps (fun _ -> current_sign) env in
-  start_proof nas Declare.NeverDischarge env' concl;
-  begin 
-    try
-      by (tclCOMPLETE (tclTHEN (tclDO (sign_length sign) intro) tac)); 
-      save_named true
-    with e when catchable_exception e -> 
-      (abort_current_proof(); raise e)
-  end;
-  exact (applist ((Declare.construct_reference env' CCI na),
-                  (List.map (fun id -> VAR(id)) 
-                     (List.rev (ids_of_sign sign)))))
+  let lemme =
+    start_proof na Declare.NeverDischarge env' concl;
+    let _,(const,strength) =
+      try
+	by (tclCOMPLETE (tclTHEN (tclDO (sign_length sign) intro) tac)); 
+	release_proof ()
+      with e when catchable_exception e -> 
+	(abort_current_proof(); raise e)
+    in   (* Faudrait un peu fonctionnaliser cela *)
+    Declare.declare_constant na (const,strength);
+    let newenv = Global.env() in
+    Declare.construct_reference newenv CCI na
+  in
+  exact (applist (lemme,
+		  List.map (fun id -> VAR id) (List.rev (ids_of_sign sign))))
     gls
 
 let tclABSTRACT name_op tac gls = 
   let s = match name_op with 
     | Some s -> s 
-    | None   -> id_of_string ((get_current_proof_name ())^"_subproof") 
+    | None   -> id_of_string
+	((string_of_id (get_current_proof_name ()))^"_subproof") 
   in  
   abstract_subproof s tac gls
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9c56db03a5..49d6bf7b20 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -367,9 +367,34 @@ let build_scheme lnamedepindsort =
   List.iter2 declare listdecl lrecnames; 
   if is_verbose() then pPNL(recursive_message lrecnames)
 
-let start_proof_com s stre com =
+let start_proof_com sopt stre com =
   let env = Global.env () in
-  Pfedit.start_proof s stre env (interp_type Evd.empty env com)
+  let id = match sopt with
+    | Some id -> id
+    | None ->
+	next_ident_away (id_of_string "Unnamed_thm")
+	  (Pfedit.get_all_proof_names ())
+  in
+  Pfedit.start_proof id stre env (interp_type Evd.empty env com)
+
+let save_named opacity =
+  let id,(const,strength) = Pfedit.release_proof () in
+  declare_constant id (const,strength);
+  if Options.is_verbose() then message ((string_of_id id) ^ " is defined")
+
+let save_anonymous opacity save_ident strength =
+  let id,(const,_) = Pfedit.release_proof () in
+  if atompart_of_id id <> "Unnamed_thm" then
+    message("Overriding name "^(string_of_id id)^" and using "^save_ident);
+  declare_constant (id_of_string save_ident) (const,strength);
+  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)
 
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index dd41759e03..fb9071d0f7 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -38,6 +38,22 @@ val build_corecursive :  (identifier * Coqast.t * Coqast.t) list -> unit
 
 val build_scheme : (identifier * bool * identifier * Coqast.t) list -> unit
 
-val start_proof_com : string -> strength -> Coqast.t -> unit
+val start_proof_com : identifier option -> strength -> 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
 
 val get_current_context : unit -> Proof_type.evar_declarations * Environ.env
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index fcc7da2c2c..9b7250a4eb 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -164,7 +164,7 @@ let valid_buffer_loc ib dloc (b,e) =
  * or after a Drop. *)
 let make_prompt () =
   if Pfedit.refining () then
-    (Pfedit.get_current_proof_name ())^" < "
+    (Names.string_of_id (Pfedit.get_current_proof_name ()))^" < "
   else "Coq < "
 
 let top_buffer =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3e5cf4903d..74c6440d89 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -340,7 +340,7 @@ let _ =
        | [VARG_CONSTR com] ->
 	   (fun () ->
               if not (refining()) then begin
-              	start_proof_com "Unnamed_thm" NeverDischarge com;
+              	start_proof_com None NeverDischarge com;
 		if not (is_silent()) then show_open_subgoals ()
               end else 
 		error "repeated Goal not permitted in refining mode")
@@ -352,8 +352,8 @@ let _ =
     (function 
        | [VARG_IDENTIFIER id] -> 
 	   (fun () -> 
-	      let s = string_of_id id in
-	      abort_proof s; message ("Goal "^s^" aborted"))
+	      abort_proof id;
+	      message ("Goal "^(string_of_id id)^" aborted"))
        | [] -> (fun () -> 
 		  abort_current_proof ();
 		  message "Current goal aborted")
@@ -387,7 +387,7 @@ let _ =
   add "RESUME"
     (function 
        | [VARG_IDENTIFIER id] ->
-	   (fun () -> resume_proof (string_of_id id))
+	   (fun () -> resume_proof id)
        | [] -> (fun () -> resume_last_proof ())
        | _  -> bad_vernac_args "RESUME")
 
@@ -614,7 +614,7 @@ let _ =
     (function [] ->
        (fun () ->
 	  let l = Pfedit.get_all_proof_names() in 
-	  mSGNL (prlist_with_sep pr_spc pr_str l))
+	  mSGNL (print_idl l))
        | _  -> bad_vernac_args "ShowProofs")
 
 let _ =
@@ -678,7 +678,7 @@ let _ =
            in 
 	   fun () ->
              begin
-               start_proof_com (string_of_id s) stre com;
+               start_proof_com (Some s) stre com;
                if (not(is_silent())) then show_open_subgoals()
              end
        | _ -> bad_vernac_args "StartProof")
@@ -708,7 +708,7 @@ let _ =
               try
             	States.with_heavy_rollback
 		  (fun () ->
-                     start_proof_com (string_of_id s) stre com;
+                     start_proof_com (Some s) stre com;
                      if not (is_silent()) then show_open_subgoals();
                      List.iter Vernacinterp.call calls;
                      if not (is_silent()) then show_script();
@@ -719,7 +719,7 @@ let _ =
                   mSGNL [< 'sTR"Error: checking of theorem " ; print_id s ;
                            'sPC ; 'sTR"failed" ;
                            'sTR"... converting to Axiom" >];
-                  abort_proof (string_of_id s);
+                  abort_proof s;
                   parameter_def_var (string_of_id s) com
            	end else 
 		  errorlabstrm "vernacentries__TheoremProof"