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

12 files changed, 14 insertions, 118 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 5b1ad1981..e79245b0e 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -836,9 +836,7 @@ and we want to backtrack to a state labeled by:
 
 We have to perform \verb!Backtrack 32 12 2! , i.e. perform 2
 \texttt{Abort}s (to cancel goal4 and goal3), then rewind proof until
-state 12 and finally go back to environment state 32. Notice that this
-supposes that proofs are nested in a regular way (no \texttt{Resume} or
-\texttt{Suspend} commands).
+state 12 and finally go back to environment state 32.
 
 \begin{Variants}
 \item {\tt BackTo n}. \comindex{BackTo}\\
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 4fa845310..884a1e6e7 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -34,9 +34,6 @@ isomorphism} \cite{How80,Bar91,Gir89,Hue89}, \Coq~ stores proofs as
 terms of {\sc Cic}. Those terms are called {\em proof
   terms}\index{Proof term}.
 
-It is possible to edit several proofs in parallel: see Section
-\ref{Resume}.
-
 \ErrMsg When one attempts to use a proof editing command out of the
 proof editing mode, \Coq~ raises the error message : \errindex{No focused
   proof}.
@@ -174,35 +171,6 @@ proof was edited.
 \end{Variants}
 
 %%%%
-\subsection[\tt Suspend.]{\tt Suspend.\comindex{Suspend}}
-
-This command applies in proof editing mode. It switches back to the
-\Coq\ toplevel, but without canceling the current proofs.
-
-%%%%
-\subsection[\tt Resume.]{\tt Resume.\comindex{Resume}\label{Resume}}
-
-This commands switches back to the editing of the last edited proof.
-
-\begin{ErrMsgs}
-\item \errindex{No proof-editing in progress}
-\end{ErrMsgs}
-
-\begin{Variants}
-
-\item {\tt Resume {\ident}.}
-
-  Restarts the editing of the proof named {\ident}. This can be used
-  to navigate between currently edited proofs.
-
-\end{Variants}
-
-\begin{ErrMsgs}
-\item \errindex{No such proof}
-\end{ErrMsgs}
-
-
-%%%%
 \subsection[\tt Existential {\num} := {\term}.]{\tt Existential  {\num} := {\term}.\comindex{Existential}
 \label{Existential}}
 
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index b9e141455..256426d22 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -127,7 +127,6 @@ let commands = [
      "Show Script";
      "Show Tree";*)
      "Structure";
-     (* "Suspend"; *)
      "Syntactic Definition";
      "Syntax";];
   [
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 9abb8cd17..385161980 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -58,9 +58,6 @@ GEXTEND Gram
       | IDENT "Defined" -> VernacEndProof (Proved (false,None))
       |	IDENT "Defined"; id=identref ->
 	  VernacEndProof (Proved (false,Some (id,None)))
-      | IDENT "Suspend" -> VernacSuspend
-      | IDENT "Resume" -> VernacResume None
-      | IDENT "Resume"; id = identref -> VernacResume (Some id)
       | IDENT "Restart" -> VernacRestart
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index b569d2fa6..c4ffbfd15 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -442,11 +442,9 @@ let rec pr_vernac = function
   (* Proof management *)
   | VernacAbortAll -> str "Abort All"
   | VernacRestart -> str"Restart"
-  | VernacSuspend -> str"Suspend"
   | VernacUnfocus -> str"Unfocus"
   | VernacGoal c -> str"Goal" ++ pr_lconstrarg c
   | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
-  | VernacResume id -> str"Resume" ++ pr_opt pr_lident id
   | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i
   | VernacUndoTo i -> str"Undo" ++ spc() ++ str"To" ++ pr_intarg i
   | VernacBacktrack (i,j,k) ->
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 02401dc03..731560386 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 fc2b25184..ceed54696 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 398e5d949..c6bb5e449 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 53aab2b9d..8dbb63739 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
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 7f01f0307..f92dcdb08 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -195,8 +195,6 @@ let rec attribute_of_vernac_command = function
   | VernacAbort _ -> []
   | VernacAbortAll -> [NavigationCommand]
   | VernacRestart -> [NavigationCommand]
-  | VernacSuspend -> [NavigationCommand]
-  | VernacResume _ -> [NavigationCommand]
   | VernacUndo _ -> [NavigationCommand]
   | VernacUndoTo _ -> [NavigationCommand]
   | VernacBacktrack _ -> [NavigationCommand]
@@ -338,7 +336,7 @@ let rewind count =
     in
     (* 3) Now that [target.proofs] is a subset of the opened proofs before
        the rewind, we simply abort the extra proofs (if any).
-       NB: It is critical here that proofs are nested in a regular way
+       NB: It is critical here that proofs are nested in a regular way.
        (i.e. no Resume or Suspend, as enforced above). This way, we can simply
        count the extra proofs to abort instead of taking care of their names.
     *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 22c89cee6..12508d754 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1345,12 +1345,6 @@ let vernac_restart () = restart_proof(); print_subgoals ()
 
   (* Proof switching *)
 
-let vernac_suspend = suspend_proof
-
-let vernac_resume = function
-  | None -> resume_last_proof ()
-  | Some id -> resume_proof id
-
 let vernac_undo n =
   undo n;
   print_subgoals ()
@@ -1554,8 +1548,6 @@ let interp c = match c with
   | VernacAbort id -> vernac_abort id
   | VernacAbortAll -> vernac_abort_all ()
   | VernacRestart -> vernac_restart ()
-  | VernacSuspend -> vernac_suspend ()
-  | VernacResume id -> vernac_resume id
   | VernacUndo n -> vernac_undo n
   | VernacUndoTo n -> undo_todepth n
   | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index e49cd3b66..d77349bc5 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -348,8 +348,6 @@ type vernac_expr =
   | VernacAbort of lident option
   | VernacAbortAll
   | VernacRestart
-  | VernacSuspend
-  | VernacResume of lident option
   | VernacUndo of int
   | VernacUndoTo of int
   | VernacBacktrack of int*int*int