From 9a822a9b927bb3516445779f7de99cf0ef43692e Mon Sep 17 00:00:00 2001
From: pboutill
Date: Wed, 5 May 2010 11:53:24 +0000
Subject: 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
---
 ide/coq.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'ide')

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))
-- 
cgit v1.2.3