Achèvement nettoyage Pfedit

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

2 files changed, 46 insertions, 21 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 44c4fc5fb7..7b1794c154 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -18,6 +18,11 @@ open Proof_type
 open Lib
 open Astterm
 
+(*********************************************************************)
+(* Managing the proofs state                                         *)
+(* Mainly contributed by C. Murthy                                   *)
+(*********************************************************************)
+
 type proof_topstate = {
   top_hyps : env * env;
   top_goal : goal;
@@ -84,12 +89,21 @@ let set_current_proof s =
   with Invalid_argument "Edit.focus" ->
     errorlabstrm "Pfedit.set_proof"
       [< 'sTR"No such proof" ; (msg_proofs false) >]
+
+let resume_proof = set_current_proof
+
+let suspend_proof () =
+  try 
+    Edit.unfocus proof_edits
+  with Invalid_argument "Edit.unfocus" ->
+    errorlabstrm "Pfedit.suspend_current_proof"
+      [< 'sTR"No active proof" ; (msg_proofs true) >]
       
 let resume_last_proof () =
   match (Edit.last_focused proof_edits) with
     | None ->
         errorlabstrm "resume_last" [< 'sTR"No proof-editing in progress." >]
-    | p -> 
+    | Some p -> 
 	Edit.focus proof_edits p
 	  
 let get_current_proof_name () =
@@ -122,7 +136,7 @@ let start (na,ts) =
   let pfs = mk_pftreestate ts.top_goal in 
   add_proof(na,pfs,ts)
     
-let restart () =
+let restart_proof () =
   match Edit.read proof_edits with
     | None -> 
 	errorlabstrm "Pfedit.restart"
@@ -130,7 +144,7 @@ let restart () =
     | Some(na,_,ts) -> 
 	del_proof na;
         start (na,ts);
-        set_current_proof (Some na)
+        set_current_proof na
 
 let proof_term () =
   extract_pftreestate (get_pftreestate())
@@ -217,11 +231,11 @@ let check_no_pending_proofs () =
       [< 'sTR"Proof editing in progress" ; (msg_proofs false) ;
          'sTR"Use \"Abort All\" first or complete proof(s)." >]
 
-let abort_goal pn = del_proof pn
+let abort_proof = del_proof
 
-let abort_current_goal () = del_proof (get_current_proof_name ())
+let abort_current_proof () = del_proof (get_current_proof_name ())
 
-let abort_goals = init_proofs
+let abort_all_proofs = init_proofs
    
 (*********************************************************************)
 (*              Modifying the current prooftree                      *)
@@ -235,7 +249,7 @@ let start_proof na str env concl =
     top_strength = str }
   in
   start(na,ts);
-  set_current_proof (Some na)
+  set_current_proof na
 
 (*
 let start_proof_constr na str concl =
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 6d5c56439a..7f9954b800 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -12,6 +12,13 @@ open Proof_type
 open Tacmach
 (*i*)
 
+(*s Several proofs can be opened simultaneously but at most one is
+   focused at some time. The following functions work by side-effect
+   on current set of open proofs. In this module, ``proofs'' means an
+   open proof (something started by vernacular command [Goal], [Lemma]
+   or [Theorem], and ``goal'' means a subgoal of the current focused
+   proof *)
+
 (* [refining ()] tells if there is some proof in progress, even if a not
    focused one *)
 
@@ -22,19 +29,19 @@ val refining : unit -> bool
 
 val check_no_pending_proofs : unit -> unit
 
-(* [abort_goal name] aborts proof of name [name] or failed if no proof
+(* [abort_proof name] aborts proof of name [name] or failed if no proof
 has this name *)
 
-val abort_goal : string -> unit
+val abort_proof : string -> unit
 
-(* [abort_current_goal ()] aborts current focused proof or failed if
+(* [abort_current_proof ()] aborts current focused proof or failed if
     no proof is focused *)
 
-val abort_current_goal : unit -> unit
+val abort_current_proof : unit -> unit
 
-(* [abort_goals ()] aborts all open proofs if any *)
+(* [abort_all_proofs ()] aborts all open proofs if any *)
 
-val abort_goals : unit -> unit
+val abort_all_proofs : unit -> unit
 
 (* [undo n] undoes the effect of the last [n] tactics applied to the
     current proof; it fails if no proof is focused or if the ``undo''
@@ -71,25 +78,29 @@ val get_goal_context : int -> evar_declarations * env
 
 val get_current_goal_context : unit -> evar_declarations * env
 
-(* [set_current_proof None] unfocuses the current focused proof; [set_proof
-(Some name)] focuses on the proof of name [name] or raises a
-[UserError] if no proof has name [name] *)
+(* [resume_proof name] focuses on the proof of name [name] or
+   raises [UserError] if no proof has name [name] *)
+
+val resume_proof : string -> unit
+
+(* [suspend_proof ()] unfocuses the current focused proof or
+   failed with [UserError] if no proof is currently focused *)
 
-val set_current_proof : string option -> unit
+val suspend_proof : unit -> unit
 
 (* [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
 
-(* [list_proofs ()] returns the list of all pending proof names *)
+(* [get_all_proof_names ()] returns the list of all pending proof names *)
 
 val get_all_proof_names : unit -> string list
 
-(* [restart ()] restarts the current focused proof from the beginning
+(* [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
 
-val restart : unit -> unit
+val restart_proof : unit -> unit
 
 (* [start_proof s str env t] starts a proof of name [s] and conclusion [t] *)
 
@@ -130,7 +141,7 @@ val by : tactic -> unit
 
 val instantiate_nth_evar_com : int -> Coqast.t -> unit
 
-(* To deal with focus *)
+(* To deal with subgoal focus *)
 
 val make_focus : int -> unit
 val focus : unit -> int