Bug résiduel du backtrack de coqide se produisant lorsque la limite de

la pile de undo de tactique est atteinte (il ne fallait pas oublier de
faire un abort). On en profite pour porter cette limite à une valeur
significativement plus élevée.


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

3 files changed, 58 insertions, 35 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 44dac6a94..61e223875 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -44,6 +44,8 @@ let init () =
      messages *)
 (**)
   Flags.make_silent true;
+  (* don't set a too large undo stack because Edit.create allocates an array *)
+  Pfedit.set_undo (Some 5000);
 (**)
   Coqtop.init_ide ()
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 47ab9f1d9..353cf304b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -543,8 +543,11 @@ type backtrack =
 | NoBacktrack
 
 let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x
-let add_abort = function (n,a,b,0,l) -> (0,a+1,b,0,l) | (n,a,b,p,l) -> (n,a,b,p-1,l)
-let add_qed q (n,a,b,p,l) = (n,a,b,p+q,l)
+let add_abort = function
+  | (n,a,b,0,l) -> (0,a+1,b,0,l)
+  | (n,a,b,p,l) -> (n,a,b,p-1,l)
+let add_qed q (n,a,b,p,l as x) =
+  if q = 0 then x else (n,a,BacktrackToNextActiveMark,p+q,l)
 let add_backtrack (n,a,b,p,l) b' = (n,a,b',p,l)
 
 let update_proofs (n,a,b,p,cur_lems) prev_lems =
@@ -580,38 +583,46 @@ let pop_command undos t =
   ignore (pop ());
   undos
 
-let rec apply_backtrack l = function
-  | 0, BacktrackToMark mark -> reset_to mark
-  | 0, NoBacktrack -> ()
-  | 0, BacktrackToModSec id -> reset_to_mod id
-  | p, _ ->
-      (* re-synchronize Coq to the current state of the stack *)
-      if is_empty () then
-        Coq.reset_initial ()
-      else
-        begin
-          let t = top () in
-          let undos = (0,0,BacktrackToNextActiveMark,p,l) in
-          let (_,_,b,p,l) = pop_command undos t in
-          apply_backtrack l (p,b);
-          let reset_info = Coq.compute_reset_info (snd t.ast) in
-          interp_last t.ast;
-          repush_phrase reset_info t
-        end
-
-let rec apply_undos (n,a,b,p,l) =
-  (* Aborts *)
+let apply_aborts a =
   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 
+  try Util.repeat a Pfedit.delete_current_proof ()
+  with e -> prerr_endline "WARNING : found a closed environment"; raise e
+
+exception UndoStackExhausted
+
+let apply_tactic_undo n =
+  if n<>0 then
     (prerr_endline ("Applying "^string_of_int n^" undos");
-     try Pfedit.undo n
-     with _ -> (* Undo stack exhausted *)
-       apply_backtrack l (p,BacktrackToNextActiveMark));
-  (* Reset *)
-  apply_backtrack l (p,b)
+     try Pfedit.undo n with _ -> raise UndoStackExhausted)
+
+let apply_reset = function
+  | BacktrackToMark mark -> reset_to mark
+  | BacktrackToModSec id -> reset_to_mod id
+  | NoBacktrack -> ()
+  | BacktrackToNextActiveMark -> assert false
+
+let rec apply_undos (n,a,b,p,l as undos) =
+  if p = 0 & b <> BacktrackToNextActiveMark then
+    begin
+      apply_aborts a;
+      try
+	apply_tactic_undo n;
+	apply_reset b
+      with UndoStackExhausted ->
+	apply_undos (n,0,BacktrackToNextActiveMark,p,l)
+    end
+  else
+    (* re-synchronize Coq to the current state of the stack *)
+    if is_empty () then
+      Coq.reset_initial ()
+    else
+      begin
+        let t = top () in
+        apply_undos (pop_command undos t);
+        let reset_info = Coq.compute_reset_info (snd t.ast) in
+        interp_last t.ast;
+        repush_phrase reset_info t
+      end
 
 (* For electric handlers *)
 exception Found
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 8501b3436..deedf957d 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -23,6 +23,16 @@ open Nametab
 
 let local_make_qualid l id = make_qualid (make_dirpath l) id
 
+let my_int_of_string loc s =
+  try
+    let n = int_of_string s in
+    (* To avoid Array.make errors (that e.g. Undo uses), we set a *)
+    (* more restricted limit than int_of_string does *)
+    if n > 1024 * 2048 then raise Exit;
+    n
+  with Failure _ | Exit ->
+    Util.user_err_loc (loc,"",Pp.str "cannot support a so large number.")
+
 GEXTEND Gram
   GLOBAL: 
     bigint natural integer identref name ident var preident
@@ -90,11 +100,11 @@ GEXTEND Gram
     [ [ s = STRING -> s ] ]
   ;
   integer:
-    [ [ i = INT      -> int_of_string i
-      | "-"; i = INT -> - int_of_string i ] ]
+    [ [ i = INT      -> my_int_of_string loc i
+      | "-"; i = INT -> - my_int_of_string loc i ] ]
   ;
   natural:
-    [ [ i = INT -> int_of_string i ] ]
+    [ [ i = INT -> my_int_of_string loc i ] ]
   ;
   bigint: (* Negative numbers are dealt with specially *)
     [ [ i = INT -> (Bigint.of_string i) ] ]