Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof

- ide doesn't crash anymore at any backtrack
- I don't see if vernacentries.ml did the same assumption so I didn't
  change anything. (The only other use of resume_proof)

- ide still raises "NoCurrentProof" when you type a bad keyword such as
  "Priint"... But at least, this on is catch somewhere !

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

3 files changed, 22 insertions, 16 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index b1e8572bd3..274d9e46b0 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -360,13 +360,15 @@ let rewind coqtop count =
         Hashtbl.iter
           (fun id depth ->
              if List.mem id prev_proofs then begin
-               Pfedit.resume_proof (Util.dummy_loc,id);
+               Pfedit.suspend_proof ();
+	       Pfedit.resume_proof (Util.dummy_loc,id);
                Pfedit.undo_todepth depth
              end)
           undo_ops;
         prerr_endline "OK for undos";
         Option.iter (fun id -> if List.mem id prev_proofs then
-                       Pfedit.resume_proof (Util.dummy_loc,id)) curprf;
+                       Pfedit.suspend_proof ();
+		       Pfedit.resume_proof (Util.dummy_loc,id)) curprf;
         prerr_endline "OK for focusing";
         List.iter
           (fun id -> Pfedit.delete_proof (Util.dummy_loc,id))
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 112003e8de..f95721a7a9 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -96,7 +96,9 @@ val restart_proof : unit -> unit
 val resume_last_proof : unit -> unit
 
 (** [resume_proof name] focuses on the proof of name [name] or
-   raises [UserError] if no proof has name [name] *)
+   raises [NoSuchProof] if no proof has name [name]. 
+
+    It doesn't [suspend_proof ()] before. *)
 
 val resume_proof : identifier located -> unit
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 40908dfc44..c7b836a518 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -6,24 +6,22 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(***********************************************************************)
-(*                                                                     *)
-(*      This module defines the global proof environment               *)
-(*      Especially it keeps tracks of whether or not there is          *)
-(*      a proof which is currently being edited.                       *)
-(*                                                                     *)
-(***********************************************************************)
-
-(* Type of proof modes :
+(** This module defines the global proof environment
+
+ Especially it keeps tracks of whether or not there is a proof which is currently being edited. *)
+
+(** Type of proof modes :
     - A name
     - A function [set] to set it *from standard mode*
-    - A function [reset] to reset the *standard mode* from it *)
+    - A function [reset] to reset the *standard mode* from it 
+
+*)
 type proof_mode = {
   name : string ;
   set : unit -> unit ;
   reset : unit -> unit
 }
-(* Registers a new proof mode which can then be adressed by name
+(** Registers a new proof mode which can then be adressed by name
     in [set_default_proof_mode].
     One mode is already registered - the standard mode - named "No",
     It corresponds to Coq default setting are they are set when coqtop starts. *)
@@ -40,7 +38,7 @@ val discard : Names.identifier Util.located -> unit
 val discard_current : unit -> unit
 val discard_all : unit -> unit
 
-(* [set_proof_mode] sets the proof mode to be used after it's called. It is
+(** [set_proof_mode] sets the proof mode to be used after it's called. It is
     typically called by the Proof Mode command. *)
 val set_proof_mode : string -> unit
 
@@ -48,7 +46,7 @@ exception NoCurrentProof
 val give_me_the_proof : unit -> Proof.proof
 
 
-(* [start_proof s str goals ~init_tac ~compute_guard hook] starts 
+(** [start_proof s str goals ~init_tac ~compute_guard hook] starts 
     a proof of name [s] and
     conclusion [t]; [hook] is optionally a function to be applied at
     proof end (e.g. to declare the built constructions as a coercion
@@ -68,9 +66,13 @@ val close_proof : unit ->
 			    Decl_kinds.goal_kind * 
 			    Tacexpr.declaration_hook)
 
+exception NoSuchProof
+
 val suspend : unit -> unit
 val resume_last : unit -> unit
+
 val resume : Names.identifier -> unit
+(** @raise NoSuchProof if it doesn't find *)
 
 (* Runs a tactic on the current proof. Raises [NoCurrentProof] is there is 
    no current proof. *)