Remove old proof-managment commands Suspend/Resume

There're not compatible with the current Backtrack mecanism used
both by ProofGeneral and CoqIDE.

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

4 files changed, 12 insertions, 64 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 02401dc03e..7315603861 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -69,10 +69,6 @@ let start_proof id str hyps c ?init_tac ?compute_guard hook =
 
 let restart_proof () = undo_todepth 1
 
-let resume_last_proof () = Proof_global.resume_last ()
-let resume_proof (_,id) = Proof_global.resume id
-let suspend_proof ()  =  Proof_global.suspend ()
-
 let cook_proof hook =
   let prf = Proof_global.give_me_the_proof () in
   hook prf;
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index fc2b251845..ceed54696c 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -86,24 +86,6 @@ val start_proof :
 val restart_proof : unit -> unit
 
 (** {6 ... } *)
-(** [resume_last_proof ()] focus on the last unfocused proof or fails
-   if there is no suspended proofs *)
-
-val resume_last_proof : unit -> unit
-
-(** [resume_proof name] focuses on the proof of name [name] or
-   raises [NoSuchProof] if no proof has name [name]. 
-
-    It doesn't [suspend_proof ()] before. *)
-
-val resume_proof : identifier located -> unit
-
-(** [suspend_proof ()] unfocuses the current focused proof or
-   failed with [UserError] if no proof is currently focused *)
-
-val suspend_proof : unit -> unit
-
-(** {6 ... } *)
 (** [cook_proof opacity] turns the current proof (assumed completed) into
     a constant with its name, kind and possible hook (see [start_proof]);
     it fails if there is no current proof of if it is not completed;
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 398e5d9497..c6bb5e449e 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -70,12 +70,10 @@ type proof_info = {
   mode : proof_mode
 }
 
-(* Invariant: a proof is at most in one of current_proof and suspended. And the
-   domain of proof_info is the union of that of current_proof and suspended.*)
-(* The head of [!current_proof] is the actual current proof, the other ones are to
-    be resumed when the current proof is closed, aborted or suspended. *)
+(* Invariant: the domain of proof_info is current_proof.*)
+(* The head of [!current_proof] is the actual current proof, the other ones are
+   to be resumed when the current proof is closed or aborted. *)
 let current_proof = ref ([]:nproof list)
-let suspended = ref ([] : nproof list)
 let proof_info = ref (Idmap.empty : proof_info Idmap.t)
 
 (* Current proof_mode, for bookkeeping *)
@@ -93,7 +91,7 @@ let update_proof_mode () =
       !current_proof_mode.reset ();
       current_proof_mode := standard
 
-(* combinators for the current_proof and suspended lists *)
+(* combinators for the current_proof lists *)
 let push a l = l := a::!l;
   update_proof_mode ()
 
@@ -145,8 +143,7 @@ let remove id m =
 (*** Proof Global manipulation ***)
 
 let get_all_proof_names () =
-    List.map fst !current_proof @
-    List.map fst !suspended
+    List.map fst !current_proof
 
 let give_me_the_proof () =
   snd (find_top current_proof)
@@ -160,53 +157,33 @@ let get_current_proof_name () =
     accessed directly through vernacular commands. Error message should be
    pushed to external layers, and so we should be able to have a finer
    control on error message on complex actions. *)
-let msg_proofs use_resume =
+let msg_proofs () =
   match get_all_proof_names () with
     | [] -> (spc () ++ str"(No proof-editing in progress).")
     | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
-               (pr_sequence Nameops.pr_id l) ++
-	       str"." ++
-               (if use_resume then (fnl () ++ str"Use \"Resume\" first.")
-              	else (mt ()))
-	    )
-
+               (pr_sequence Nameops.pr_id l) ++ str".")
 
 let there_is_a_proof () = !current_proof <> []
-let there_are_suspended_proofs () = !suspended <> []
-let there_are_pending_proofs () =
-  there_is_a_proof () ||
-  there_are_suspended_proofs ()
+let there_are_pending_proofs () = there_is_a_proof ()
 let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
     ()
   else begin
     Errors.error (Pp.string_of_ppcmds
-      (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
+      (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
        str"Use \"Abort All\" first or complete proof(s)."))
   end
 
-
-let suspend () =
-  rotate_top current_proof suspended
-
-let resume_last () =
-  rotate_top suspended current_proof
-
-let resume id =
-  rotate_find id suspended current_proof
-
 let discard_gen id =
-  try
-    ignore (extract id current_proof);
-    remove id proof_info
-  with NoSuchProof -> ignore (extract id suspended)
+  ignore (extract id current_proof);
+  remove id proof_info
 
 let discard (loc,id) =
   try
     discard_gen id
   with NoSuchProof ->
     Errors.user_err_loc
-      (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
+      (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
   let (id,_) = extract_top current_proof in
@@ -214,7 +191,6 @@ let discard_current () =
 
 let discard_all () =
   current_proof := [];
-  suspended := [];
   proof_info := Idmap.empty
 
 (* [set_proof_mode] sets the proof mode to be used after it's called. It is
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 53aab2b9db..8dbb63739f 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -69,12 +69,6 @@ val close_proof : unit ->
 
 exception NoSuchProof
 
-val suspend : unit -> unit
-val resume_last : unit -> unit
-
-val resume : Names.identifier -> unit
-(** @raise NoSuchProof if it doesn't find one. *)
-
 (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is 
    no current proof. *)
 val run_tactic : unit Proofview.tactic -> unit