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

4 files changed, 53 insertions, 12 deletions

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"