diff options
| author | pboutill | 2010-05-05 11:53:24 +0000 |
|---|---|---|
| committer | pboutill | 2010-05-05 11:53:24 +0000 |
| commit | 9a822a9b927bb3516445779f7de99cf0ef43692e (patch) | |
| tree | 4dbe3481df76517b3884a33f091889d70638927f /ide | |
| parent | 0583805fa794380eb9031e2c8a147fee7facacf0 (diff) | |
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
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 6 |
1 files changed, 4 insertions, 2 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)) |