Plutôt que de reposer sur le vernacexpr pour détecter les débuts de

buts, on se base sur les informations de Pfedit (comme le fait Pierre
Courtieu). Permet d'être plus robuste sur les extensions de syntaxe
ouvrant des buts, style Function.



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

3 files changed, 47 insertions, 47 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index c81318711d..521e288cd8 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -350,6 +350,19 @@ let is_vernac_tactic_command com =
 let is_vernac_proof_ending_command com =
   List.mem ProofEndingCommand (attribute_of_vernac_command com)
 
+type undo_info = int * int
+
+let open_proofs = ref [] 
+
+let undo_info () =
+  let current = Pfedit.get_all_proof_names () in
+  let common = list_intersect current !open_proofs in
+  let ncommon = List.length common in
+  let more = List.length current - ncommon in
+  let less = List.length !open_proofs - ncommon in
+  open_proofs := current;
+  (more,less)
+
 type reset_mark =
   | ResetToId of Names.identifier
   | ResetToState of Libnames.object_name
@@ -357,13 +370,14 @@ type reset_mark =
 type reset_status =
   | NoReset
   | 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
+  | Some sp -> 
+      prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
+      ResetToState sp
   | None -> ResetToId id
 
 let compute_reset_info = function 
@@ -381,13 +395,12 @@ let compute_reset_info = function
   | com when is_vernac_proof_ending_command com -> NoReset, ref true
   | VernacEndSegment _ -> NoReset, ref true
 
-  | com when is_vernac_goal_starting_command com ->
-      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)
+      | Some sp -> 
+	  prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
+	  ResetAtRegisteredObject (ResetToState sp)
       | None -> NoReset), ref true
 
 let reset_initial () = 
diff --git a/ide/coq.mli b/ide/coq.mli
index 9c95ec0595..6208fba373 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -35,9 +35,12 @@ type reset_mark =
 type reset_status =
   | NoReset
   | ResetAtSegmentStart of Names.identifier
-  | ResetAtStatement of Libnames.object_name option
   | ResetAtRegisteredObject of reset_mark
 
+type undo_info = int * int
+
+val undo_info : unit -> undo_info
+
 type reset_info = reset_status * bool ref
 
 val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
diff --git a/ide/coqide.ml b/ide/coqide.ml
index a519f23979..4488cef045 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -491,6 +491,7 @@ type info =  {start:GText.mark;
 	      stop:GText.mark;
 	      ast:Util.loc * Vernacexpr.vernac_expr;
 	      reset_info:Coq.reset_info;
+	      undo_info:Coq.undo_info;
 	     }
 
 exception Size of int
@@ -502,18 +503,6 @@ let is_empty () = Stack.is_empty processed_stack
 
 (* push a new Coq phrase *)
 
-let update_on_end_of_proof () =
-  let lookup_lemma = function
-    | { reset_info = ResetAtRegisteredObject _, r } -> 
-	prerr_endline "Toggling Frozen State info to false";
-	r := false
-    | { reset_info = ResetAtStatement _, r } ->
-	prerr_endline "Toggling Reset info to true";
-	r := true; 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', _ } when id = id' -> raise Exit
@@ -525,11 +514,11 @@ let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast =
   let x = {start = start_of_phrase_mark;
 	   stop = end_of_phrase_mark;
 	   ast = ast;
-	   reset_info = reset_info
+	   reset_info = reset_info;
+	   undo_info = Coq.undo_info ()
 	  } in
   begin
     match snd ast with
-    | com when is_vernac_proof_ending_command com -> update_on_end_of_proof ()
     | VernacEndSegment (_,id) -> update_on_end_of_segment id
     | _ -> ()
   end;
@@ -537,10 +526,9 @@ let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast =
 
 
 let repush_phrase reset_info x =
-  let x = { x with reset_info = reset_info } in
+  let x = { x with reset_info = reset_info; undo_info = Coq.undo_info () } in
   begin
     match snd x.ast with
-      | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof ()
       | VernacEndSegment (_,id) -> update_on_end_of_segment id
       | _ -> ()
   end;
@@ -554,34 +542,30 @@ type backtrack =
 
 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_qed q (n,a,b,p) = (n,a,b,p+q)
 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 =
-    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
-    | {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, _} ->
-        add_backtrack undos (BacktrackToModSec id)
-    | {reset_info=ResetAtStatement (Some st), _} ->
-        add_proof_start undos (BacktrackToMark (ResetToState st))
-    | {ast=(_,com)} ->
-        add_backtrack undos BacktrackToNextActiveMark in
+    if !(snd t.reset_info) then
+      let (openproofs,closedproofs) = t.undo_info in
+      let undos = Util.iterate add_abort openproofs undos in
+      let undos = add_qed closedproofs undos in
+      match fst t.reset_info with
+      | _ when is_vernac_tactic_command (snd t.ast) ->
+	  (* A tactic, active if not below a Qed *)
+          add_undo undos
+      | ResetAtRegisteredObject mark ->
+          add_backtrack undos (BacktrackToMark mark)
+      | ResetAtSegmentStart id ->
+          add_backtrack undos (BacktrackToModSec id)
+      | _ when is_vernac_state_preserving_command (snd t.ast) ->
+	  undos
+      | _ ->
+          add_backtrack undos BacktrackToNextActiveMark
+    else
+      (* An object inside a closed section *)
+      add_backtrack undos BacktrackToNextActiveMark in
   ignore (pop ());
   undos