Achèvement nettoyage Pfedit

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

5 files changed, 77 insertions, 42 deletions

diff --git a/lib/edit.ml b/lib/edit.ml
index ae54d71da5..8d0b0aa276 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -15,24 +15,32 @@ let empty () = {
   buf = Hashtbl.create 17 }
 
 let focus e nd =
-  begin match nd with
-    | None -> ()
-    | Some f -> if not (Hashtbl.mem e.buf f) then invalid_arg "Edit.focus"
-  end;
+  if not (Hashtbl.mem e.buf nd) then invalid_arg "Edit.focus";
   begin match e.focus with
-    | None -> if nd = None then warning "There is already no focused proof"
-    | Some foc -> 
-	if e.focus <> nd then
-          e.last_focused_stk <- foc::(list_except foc e.last_focused_stk)
+    | Some foc when foc <> nd ->
+        e.last_focused_stk <- foc::(list_except foc e.last_focused_stk);
+    | _ -> ()
   end;
-  e.focus <- nd
+  e.focus <- Some nd
+
+let unfocus e =
+  match e.focus with
+    | None -> invalid_arg "Edit.unfocus"
+    | Some foc ->
+	begin
+	  e.last_focused_stk <- foc::(list_except foc e.last_focused_stk);
+	  e.focus <- None
+	end
     
 let last_focused e =
   match e.last_focused_stk with
     | [] -> None
     | f::_ -> Some f
 
-let restore_last_focus e = focus e (last_focused e)
+let restore_last_focus e =
+  match e.last_focused_stk with
+    | [] -> ()
+    | f::_ -> focus e f
 			     
 let focusedp e =
   match e.focus with
diff --git a/lib/edit.mli b/lib/edit.mli
index 6d5744259d..5926456f0a 100644
--- a/lib/edit.mli
+++ b/lib/edit.mli
@@ -13,9 +13,11 @@ type ('a,'b,'c) t
 
 val empty : unit -> ('a,'b,'c) t
 
-(* sets the focus to the specified domain element, or if [None],
- * unsets the focus *)
-val focus : ('a,'b,'c) t -> 'a option -> unit
+(* sets the focus to the specified domain element *)
+val focus : ('a,'b,'c) t -> 'a -> unit
+
+(* unsets the focus which must not already be unfocused *)
+val unfocus : ('a,'b,'c) t -> unit
 
 (* gives the last focused element or [None] if none *)
 val last_focused : ('a,'b,'c) t -> 'a option
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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f21768913e..f90af433bb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -214,7 +214,7 @@ let _ =
 (* Managing states *)
 
 let abort_refine f x =
-  if Pfedit.refining() then abort_goals ();
+  if Pfedit.refining() then abort_all_proofs ();
   f x
   (* used to be: error "Must save or abort current goal first" *)
 
@@ -353,9 +353,9 @@ let _ =
        | [VARG_IDENTIFIER id] -> 
 	   (fun () -> 
 	      let s = string_of_id id in
-	      abort_goal s; message ("Goal "^s^" aborted"))
+	      abort_proof s; message ("Goal "^s^" aborted"))
        | [] -> (fun () -> 
-		  abort_current_goal ();
+		  abort_current_proof ();
 		  message "Current goal aborted")
        | _  -> bad_vernac_args "ABORT")
 
@@ -364,7 +364,7 @@ let _ =
     (function 
        | [] -> (fun () ->
 		  if refining() then begin
-		    abort_goals ();
+		    abort_all_proofs ();
 		    message "Current goals aborted"
 		  end else
 		    error "No proof-editing in progress")
@@ -374,20 +374,20 @@ let _ =
 let _ =
   add "RESTART"
     (function 
-       | [] -> (fun () -> (restart();show_open_subgoals ()))
+       | [] -> (fun () -> (restart_proof();show_open_subgoals ()))
        | _  -> bad_vernac_args "RESTART")
 
 let _ =
   add "SUSPEND"
     (function 
-       | [] -> (fun () -> set_current_proof None)
+       | [] -> (fun () -> suspend_proof ())
        | _  -> bad_vernac_args "SUSPEND")
 
 let _ =
   add "RESUME"
     (function 
        | [VARG_IDENTIFIER id] ->
-	   (fun () -> set_current_proof (Some(string_of_id id)))
+	   (fun () -> resume_proof (string_of_id id))
        | [] -> (fun () -> resume_last_proof ())
        | _  -> bad_vernac_args "RESUME")
 
@@ -719,7 +719,7 @@ let _ =
                   mSGNL [< 'sTR"Error: checking of theorem " ; print_id s ;
                            'sPC ; 'sTR"failed" ;
                            'sTR"... converting to Axiom" >];
-                  abort_goal (string_of_id s);
+                  abort_proof (string_of_id s);
                   parameter_def_var (string_of_id s) com
            	end else 
 		  errorlabstrm "vernacentries__TheoremProof"