Fix backtracking bugs:

 - When the undo stack overflows, backtrack within a proof goes to
   wrong state
 - Boundary checks before undoing (popping the stack) wrong


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

3 files changed, 21 insertions, 7 deletions

diff --git a/lib/bstack.ml b/lib/bstack.ml
index 52a7888849..b4232ebcf0 100644
--- a/lib/bstack.ml
+++ b/lib/bstack.ml
@@ -12,13 +12,21 @@
 
 open Util
 
+(* - size  is the count of elements actually in the queue
+   - depth is the the amount of elements pushed in the queue (and not popped)
+   in particular, depth >= size always and depth > size if the queue overflowed
+   (and forgot older elements)
+ *)
+
 type 'a t = {mutable pos : int;
              mutable size : int;
+             mutable depth : int;
              stack : 'a array}
 
 let create depth e =
   {pos = 0;
    size = 1;
+   depth = 1;
    stack = Array.create depth e}
 
 (*
@@ -37,14 +45,16 @@ let decr_pos bs =
 let push bs e =
   incr_pos bs;
   incr_size bs;
+  bs.depth <- bs.depth + 1;
   bs.stack.(bs.pos) <- e
 	  
 let pop bs =
   if bs.size > 1 then begin
     bs.size <- bs.size - 1; 
+    bs.depth <- bs.depth - 1;
     let oldpos = bs.pos in
     decr_pos bs;
-    (* Release the memory at oldpos, by coyping what is at new pos *)
+    (* Release the memory at oldpos, by copying what is at new pos *)
     bs.stack.(oldpos) <- bs.stack.(bs.pos)
   end
 
@@ -60,4 +70,6 @@ let app_repl bs f =
   if bs.size = 0 then error "Nothing on the stack"
   else bs.stack.(bs.pos) <- f (bs.stack.(bs.pos))
 
-let depth bs = bs.size
+let depth bs = bs.depth
+
+let size bs = bs.size
diff --git a/lib/bstack.mli b/lib/bstack.mli
index 0a0a26ce8f..cef8e1d9e5 100644
--- a/lib/bstack.mli
+++ b/lib/bstack.mli
@@ -19,3 +19,4 @@ val app_repl : 'a t -> ('a -> 'a) -> unit
 val pop : 'a t -> unit
 val top : 'a t -> 'a
 val depth : 'a t -> int
+val size : 'a t -> int
diff --git a/lib/edit.ml b/lib/edit.ml
index 06a55d171d..e6f2907ecc 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -80,7 +80,7 @@ let undo e n =
     | None -> invalid_arg "Edit.undo"
     | Some d ->
 	let (bs,_) = Hashtbl.find e.buf d in
-	if Bstack.depth bs = 1 & n > 0 then
+	if n >= Bstack.size bs then
 	  errorlabstrm "Edit.undo" (str"Undo stack exhausted");
         repeat n Bstack.pop bs
 
@@ -102,15 +102,16 @@ let undo_todepth e n =
 	else () (* if there is no proof in progress, then n must be zero *)
     | Some d ->
 	let (bs,_) = Hashtbl.find e.buf d in
-	if Bstack.depth bs < n then
+	let ucnt = Bstack.depth bs - n in
+	if  ucnt >= Bstack.size bs then
 	  errorlabstrm "Edit.undo_todepth" (str"Undo stack would be exhausted");
-        repeat (Bstack.depth bs - n) Bstack.pop bs
+        repeat ucnt Bstack.pop bs
 
-let create e (d,b,c,udepth) =
+let create e (d,b,c,usize) =
   if Hashtbl.mem e.buf d then
     errorlabstrm "Edit.create" 
       (str"Already editing something of that name");
-  let bs = Bstack.create udepth b in
+  let bs = Bstack.create usize b in
   Hashtbl.add e.buf d (bs,c)
 
 let delete e d =