From 32a26cd2dde0f9c31fec6952c830eb09bfb260d8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 9 Jun 2008 11:26:32 +0000
Subject: - Documentation de admit et Print Assumptions. - Relecture, mise à
 jour, correction d'erreurs et petite   réorganisation du chapitre sur les
 commandes vernaculaires. - Correction bug #1865 (rafraichissement des univers
 algébriques). - Suppression de la dépendance du initial.coq en les noms longs
 des fichiers   de façons à ce que les dépendances ne soient que purement
 logique. - Encore un (petit) bug undo ide.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coqide.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'ide')

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 73fc878b41..afef3b41ae 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -557,7 +557,7 @@ type backtrack =
 | NoBacktrack
 
 let add_undo (n,a,b) = (n+1,a,b)
-let add_abort (n,a,b) = (n,a+1,b)
+let add_abort (n,a,b) = (0,a+1,b)
 let add_backtrack (n,a,b) b' = (n,a,b')
 
 let pop_command undos t =
@@ -598,16 +598,16 @@ let rec apply_backtrack = function
         end
 
 let rec apply_undos (n,a,b) =
+  (* Aborts *)
+  if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
+  (try Util.repeat a Pfedit.delete_current_proof ()
+   with e -> prerr_endline "WARNING : found a closed environment"; raise e);
   (* Undos *)
   if n<>0 then 
     (prerr_endline ("Applying "^string_of_int n^" undos");
      try Pfedit.undo n
-     with _ -> apply_undos (n,a,BacktrackToNextActiveMark));
-  (* Aborts *)
-  if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
-  (try Util.repeat a Pfedit.delete_current_proof ()
-   with e ->
-     begin prerr_endline "WARNING : found a closed environment"; raise e end);
+     with _ -> (* Undo stack exhausted *)
+       apply_backtrack BacktrackToNextActiveMark);
   (* Reset *)
   apply_backtrack b
 
-- 
cgit v1.2.3