On prend des risques en tentant d'optimiser encore plus le undo en cas

de preuves imbriquées.



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

3 files changed, 72 insertions, 53 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index dc4594292d..c81318711d 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -184,6 +184,7 @@ let make_option_commands () =
 type command_attribute =
     NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand
   | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand
+  | ProofEndingCommand
 
 let rec attribute_of_vernac_command = function
   (* Control *)
@@ -205,8 +206,8 @@ let rec attribute_of_vernac_command = function
   | VernacDefinition (_,_,DefineBody _,_) -> []
   | VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand]
   | VernacStartTheoremProof _ -> [GoalStartingCommand]
-  | VernacEndProof _ -> []
-  | VernacExactProof _ -> []
+  | VernacEndProof _ -> [ProofEndingCommand]
+  | VernacExactProof _ -> [ProofEndingCommand]
 
   | VernacAssumption _ -> []
   | VernacInductive _ -> []
@@ -346,15 +347,20 @@ let is_vernac_state_preserving_command com =
 let is_vernac_tactic_command com =
   List.mem SolveCommand (attribute_of_vernac_command com)
 
+let is_vernac_proof_ending_command com =
+  List.mem ProofEndingCommand (attribute_of_vernac_command com)
+
 type reset_mark =
   | ResetToId of Names.identifier
-  | ResetToState of  Libnames.object_name
+  | ResetToState of Libnames.object_name
 
-type reset_info =
+type reset_status =
   | NoReset
-  | ResetAtSegmentStart of Names.identifier * bool ref 
-  | ResetAtStatement of bool ref
-  | ResetAtRegisteredObject of reset_mark * bool ref
+  | ResetAtSegmentStart of Names.identifier
+  | ResetAtStatement of Libnames.object_name option
+  | ResetAtRegisteredObject of reset_mark
+
+type reset_info = reset_status * bool ref
 
 let reset_mark id = match Lib.has_top_frozen_state () with
   | Some sp -> ResetToState sp
@@ -365,20 +371,24 @@ let compute_reset_info = function
   | VernacDefineModule (_,id, _, _, _) 
   | VernacDeclareModule (_,id, _, _)
   | VernacDeclareModuleType (id, _, _) ->
-      ResetAtSegmentStart (snd id, ref true)
+      ResetAtSegmentStart (snd id), ref true
 
   | VernacDefinition (_, (_,id), DefineBody _, _)
   | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
   | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
-      ResetAtRegisteredObject (reset_mark id, ref true)
-  | VernacEndProof _ | VernacExactProof _ | VernacEndSegment _ -> NoReset
+      ResetAtRegisteredObject (reset_mark id), ref true
+
+  | com when is_vernac_proof_ending_command com -> NoReset, ref true
+  | VernacEndSegment _ -> NoReset, ref true
+
   | com when is_vernac_goal_starting_command com ->
-      ResetAtStatement (ref false)
-  | com when is_vernac_tactic_command com -> NoReset
+      ResetAtStatement (Lib.has_top_frozen_state ()), ref false
+
+  | com when is_vernac_tactic_command com -> NoReset, ref true
   | _ ->
-      match Lib.has_top_frozen_state () with
-      | Some sp -> ResetAtRegisteredObject (ResetToState sp, ref true)
-      | None -> NoReset
+      (match Lib.has_top_frozen_state () with
+      | Some sp -> ResetAtRegisteredObject (ResetToState sp)
+      | None -> NoReset), ref true
 
 let reset_initial () = 
   prerr_endline "Reset initial called"; flush stderr;
diff --git a/ide/coq.mli b/ide/coq.mli
index cec86ab78b..9c95ec0595 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -32,11 +32,13 @@ type reset_mark =
   | ResetToId of Names.identifier
   | ResetToState of  Libnames.object_name
 
-type reset_info =
+type reset_status =
   | NoReset
-  | ResetAtSegmentStart of Names.identifier * bool ref 
-  | ResetAtStatement of bool ref
-  | ResetAtRegisteredObject of reset_mark * bool ref
+  | ResetAtSegmentStart of Names.identifier
+  | ResetAtStatement of Libnames.object_name option
+  | ResetAtRegisteredObject of reset_mark
+
+type reset_info = reset_status * bool ref
 
 val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
 val reset_initial : unit -> unit
@@ -52,6 +54,7 @@ val interp_and_replace : string ->
 val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool
 val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool
 val is_vernac_goal_starting_command : Vernacexpr.vernac_expr -> bool
+val is_vernac_proof_ending_command : Vernacexpr.vernac_expr -> bool
 
 (* type hyp = (identifier * constr option * constr) * string *)
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index afef3b41ae..aa3bc87fa8 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -504,24 +504,20 @@ let is_empty () = Stack.is_empty processed_stack
 
 let update_on_end_of_proof () =
   let lookup_lemma = function
-    | { reset_info = ResetAtRegisteredObject (_, r) } -> 
+    | { reset_info = ResetAtRegisteredObject _, r } -> 
 	prerr_endline "Toggling Frozen State info to false";
 	r := false
-    | { reset_info = ResetAtStatement r } when not !r ->
+    | { reset_info = ResetAtStatement _, r } ->
 	prerr_endline "Toggling Reset info to true";
 	r := true; raise Exit
-    | { ast = _, (VernacAbort _ | VernacAbortAll | VernacGoal _) } -> raise Exit
     | _ -> ()
   in
     try Stack.iter lookup_lemma processed_stack with Exit -> ()
 
 let update_on_end_of_segment id =
   let lookup_section = function 
-    | { reset_info = ResetAtSegmentStart (id', r) } when id = id' -> raise Exit
-    | { reset_info = ResetAtSegmentStart (_, r) } -> r := false
-    | { reset_info = ResetAtStatement r } -> r := false
-    | { reset_info = ResetAtRegisteredObject (_, r) } -> r := false
-    | _ -> ()
+    | { reset_info = ResetAtSegmentStart id', _ } when id = id' -> raise Exit
+    | { reset_info = _, r } -> r := false
   in
     try Stack.iter lookup_section processed_stack with Exit -> ()
 
@@ -533,9 +529,9 @@ let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast =
 	  } in
   begin
     match snd ast with
-      | VernacEndProof _ | VernacExactProof _ -> update_on_end_of_proof ()
-      | VernacEndSegment (_,id) -> update_on_end_of_segment id
-      | _ -> ()
+    | com when is_vernac_proof_ending_command com -> update_on_end_of_proof ()
+    | VernacEndSegment (_,id) -> update_on_end_of_segment id
+    | _ -> ()
   end;
   push x
 
@@ -556,48 +552,58 @@ type backtrack =
 | BacktrackToModSec of Names.identifier
 | NoBacktrack
 
-let add_undo (n,a,b) = (n+1,a,b)
-let add_abort (n,a,b) = (0,a+1,b)
-let add_backtrack (n,a,b) b' = (n,a,b')
+let add_undo = function (n,a,b,p as x) -> if p = 0 then (n+1,a,b,p) else x
+let add_abort = function (n,a,b,0) -> (0,a+1,b,0) | (n,a,b,p) -> (n,a,b,p-1)
+let add_qed (n,a,b,p) = (n,a,b,p+1)
+let add_backtrack (n,a,b,p) b' = (n,a,b',p)
+let add_proof_start (n,a,b,p) b' = (n,a,b',p-1)
 
 let pop_command undos t =
-  let undos = 
+  let undos =
     match t with
+    | {reset_info=ResetAtStatement _,{contents=false}} when Pfedit.refining()->
+	(* An incomplete ongoing proof *)
+        add_abort undos
+    | {reset_info=_, {contents=false}} ->
+	(* An object inside a section *)
+        add_backtrack undos BacktrackToNextActiveMark
     | {ast=(_,com)} when is_vernac_tactic_command com ->
+	(* A tactic, active if not below a Qed *)
         add_undo undos
-    | {reset_info=ResetAtRegisteredObject (mark,{contents=true})} ->
+    | {ast=(_,com)} when is_vernac_proof_ending_command com ->
+	(* Backtracking a Qed *)
+        add_qed undos
+    | {ast=(_,com)} when is_vernac_state_preserving_command com -> undos
+    | {reset_info=ResetAtRegisteredObject mark, _} ->
         add_backtrack undos (BacktrackToMark mark)
-    | {reset_info=ResetAtSegmentStart (id, {contents=true})} ->
+    | {reset_info=ResetAtSegmentStart id, _} ->
         add_backtrack undos (BacktrackToModSec id)
-    | {reset_info=ResetAtStatement {contents=false}} ->
-	prerr_endline ("Statement " ^ if Pfedit.refining () then "proof" else "none");
-        if Pfedit.refining () then add_abort undos
-        else add_backtrack undos BacktrackToNextActiveMark
+    | {reset_info=ResetAtStatement (Some st), _} ->
+        add_proof_start undos (BacktrackToMark (ResetToState st))
     | {ast=(_,com)} ->
-        if is_vernac_state_preserving_command com then undos
-        else add_backtrack undos BacktrackToNextActiveMark in
+        add_backtrack undos BacktrackToNextActiveMark in
   ignore (pop ());
   undos
 
 let rec apply_backtrack = function
-  | BacktrackToMark mark -> reset_to mark
-  | NoBacktrack -> ()
-  | BacktrackToModSec id -> reset_to_mod id
-  | BacktrackToNextActiveMark ->
+  | 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 (_,_,b) = pop_command (0,0,BacktrackToNextActiveMark) t in
-          apply_backtrack b;
+          let (_,_,b,p) = pop_command (0,0,BacktrackToNextActiveMark,p) t in
+          apply_backtrack (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) =
+let rec apply_undos (n,a,b,p) =
   (* Aborts *)
   if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
   (try Util.repeat a Pfedit.delete_current_proof ()
@@ -607,9 +613,9 @@ let rec apply_undos (n,a,b) =
     (prerr_endline ("Applying "^string_of_int n^" undos");
      try Pfedit.undo n
      with _ -> (* Undo stack exhausted *)
-       apply_backtrack BacktrackToNextActiveMark);
+       apply_backtrack (p,BacktrackToNextActiveMark));
   (* Reset *)
-  apply_backtrack b
+  apply_backtrack (p,b)
 
 (* For electric handlers *)
 exception Found
@@ -1351,7 +1357,7 @@ object(self)
         else
 	  done_smthg, undos
     in
-    let done_smthg, undos = pop_commands false (0,0,NoBacktrack) in
+    let done_smthg, undos = pop_commands false (0,0,NoBacktrack,0) in
       prerr_endline "Popped commands";
       if done_smthg then
         begin 
@@ -1420,7 +1426,7 @@ Please restart and report NOW.";
 	      self#show_goals;
 	      self#clear_message
 	    in
-              let undo = pop_command (0,0,NoBacktrack) last_command in
+              let undo = pop_command (0,0,NoBacktrack,0) last_command in
               apply_undos undo;
               sync update_input ()
 	with