Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1

This reverts commit 12537
This reverts commit 12199
This reverts commit 12198
This reverts commit 12172 (introduced the bug)

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

4 files changed, 242 insertions, 111 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 6018cc07e..ea3400f2e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -323,6 +323,9 @@ let rec attribute_of_vernac_command = function
   | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
   | VernacExtend _ -> []
 
+let is_vernac_goal_starting_command com =
+  List.mem GoalStartingCommand (attribute_of_vernac_command com)
+
 let is_vernac_navigation_command com =
   List.mem NavigationCommand (attribute_of_vernac_command com)
 
@@ -340,49 +343,74 @@ let is_vernac_goal_printing_command com =
   List.mem GoalStartingCommand attribute or
   List.mem SolveCommand attribute
 
-type reset_mark = Libnames.object_name
+let is_vernac_state_preserving_command com =
+  let attribute = attribute_of_vernac_command com in
+  List.mem OtherStatePreservingCommand attribute or
+  List.mem QueryCommand attribute
 
-type reset_info = {
-  state : reset_mark;
-  pending : identifier list;
-  pf_depth : int;
-  mutable segment : bool;
-}
+let is_vernac_tactic_command com =
+  List.mem SolveCommand (attribute_of_vernac_command com)
 
-let compute_reset_info () =
-  match Lib.has_top_frozen_state () with
-    | Some st ->
-        { state = st;
-          pending = Pfedit.get_all_proof_names ();
-          pf_depth = Pfedit.current_proof_depth ();
-          segment = true; }
-    | None ->
-        failwith "FATAL ERROR: NO RESET"
-
-type backtrack =
-  | BacktrackToNextActiveMark
-  | BacktrackToMark of reset_mark
-  | NoBacktrack
-
-type undo_cmds = {
-  n : int;
-  a : int;
-  b : backtrack;
-  p : int;
-  l : (identifier list * int);
-}
+let is_vernac_proof_ending_command com =
+  List.mem ProofEndingCommand (attribute_of_vernac_command com)
+
+type undo_info = identifier list
+
+let undo_info () = Pfedit.get_all_proof_names ()
+
+type reset_mark =
+  | ResetToId of Names.identifier     (* Relying on identifiers only *)
+  | ResetToState of Libnames.object_name (* Relying on states if any *)
+
+type reset_status =
+  | NoReset
+  | ResetAtSegmentStart of Names.identifier
+  | ResetAtRegisteredObject of reset_mark
+
+type reset_info = reset_status * undo_info * bool ref
 
-let init_undo u =
-  { n = 0; a = 0; b = NoBacktrack; p = 0;
-    l = (Pfedit.get_all_proof_names u,Pfedit.current_proof_depth u) }
+
+let reset_mark id = match Lib.has_top_frozen_state () with
+  | Some sp -> 
+      prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
+      ResetToState sp
+  | None -> ResetToId id
+
+let compute_reset_info = function 
+  | VernacBeginSection id 
+  | VernacDefineModule (_,id, _, _, _) 
+  | VernacDeclareModule (_,id, _, _)
+  | VernacDeclareModuleType (id, _, _, _) ->
+      ResetAtSegmentStart (snd id), undo_info(), ref true
+
+  | VernacDefinition (_, (_,id), DefineBody _, _)
+  | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
+  | VernacInductive (_,_, (((_,(_,id)),_,_,_,_),_) :: _) ->
+      ResetAtRegisteredObject (reset_mark id), undo_info(), ref true
+
+  | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true
+  | VernacEndSegment _ -> NoReset, undo_info(), ref true
+
+  | com when is_vernac_tactic_command com -> NoReset, undo_info(), ref true
+  | _ ->
+      (match Lib.has_top_frozen_state () with
+      | Some sp -> 
+	  prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
+	  ResetAtRegisteredObject (ResetToState sp)
+      | None -> NoReset), undo_info(), ref true
 
 let reset_initial () =
   prerr_endline "Reset initial called"; flush stderr;
   Vernacentries.abort_refine Lib.reset_initial ()
 
-let reset_to st =
-  prerr_endline ("Reset called with state "^(Libnames.string_of_path (fst st)));
-  Lib.reset_to_state st
+let reset_to = function
+  | ResetToId id ->
+      prerr_endline ("Reset called with "^(string_of_id id));
+      Lib.reset_name (Util.dummy_loc,id)
+  | ResetToState sp ->
+      prerr_endline
+        ("Reset called with state "^(Libnames.string_of_path (fst sp)));
+      Lib.reset_to_state sp
 
 let reset_to_mod id =
   prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id));
@@ -414,7 +442,7 @@ let interp_with_options verbosely options s =
 	if not (is_vernac_goal_printing_command vernac) then
 	  (* Verbose if in small step forward and not a tactic *)
 	  Flags.make_silent (not verbosely);
-	let reset_info = compute_reset_info () in
+	let reset_info = compute_reset_info vernac in
 	List.iter (fun (set_option,_) -> raw_interp set_option) options;
 	raw_interp s;
 	Flags.make_silent true;
@@ -430,6 +458,41 @@ let interp_and_replace s =
   let msg = read_stdout () in
   result,msg
 
+type bktk_info = { start : GText.mark;
+                   stop : GText.mark;
+                   state_num : int;
+                   pending_proofs : string list;
+                   proof_stack_depth : int;
+}
+
+let record_interp cmd_stk start_of_sentence end_of_sentence (sn,pp,psd) =
+  Stack.push { start = start_of_sentence;
+               stop = end_of_sentence;
+               state_num = sn;
+               pending_proofs = pp;
+               proof_stack_depth = psd;
+  } cmd_stk
+
+let backtrack cmd_stack stop_cond =
+  if Stack.is_empty cmd_stack then
+    reset_initial () (* reset coq *)
+  else try
+    let current = Stack.top cmd_stack in
+    while not (stop_cond (Stack.top cmd_stack).stop) do
+      ignore (Stack.pop cmd_stack)
+    done;
+    let target = Stack.top cmd_stack in
+    if current != target then
+      let rst = target.state_num in
+      let undo = target.proof_stack_depth in
+      let abrt = List.fold_left
+                   (fun acc e -> if List.mem e target.pending_proofs then acc else succ acc)
+                   0 current.pending_proofs
+      in
+      raw_interp (Printf.sprintf "Backtrack %d %d %d.\n" rst undo abrt)
+      else ()
+  with Stack.Empty -> reset_initial () (* might as well reset coq ... *)
+
 type tried_tactic =
   | Interrupted
   | Success of int (* nb of goals after *)
diff --git a/ide/coq.mli b/ide/coq.mli
index a03528f81..3ded7b6bd 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -29,32 +29,22 @@ type printing_state = {
 
 val printing_state : printing_state
 
-type reset_mark
+type reset_mark =
+  | ResetToId of Names.identifier
+  | ResetToState of Libnames.object_name
 
-type reset_info = {
-  state : reset_mark;
-  pending : identifier list;
-  pf_depth : int;
-  mutable segment : bool;
-}
-
-val compute_reset_info : unit -> reset_info
+type reset_status =
+  | NoReset
+  | ResetAtSegmentStart of Names.identifier
+  | ResetAtRegisteredObject of reset_mark
 
-type backtrack =
-  | BacktrackToNextActiveMark
-  | BacktrackToMark of reset_mark
-  | NoBacktrack
+type undo_info = identifier list
 
-type undo_cmds = {
-  n : int;
-  a : int;
-  b : backtrack;
-  p : int;
-  l : (identifier list * int);
-}
+val undo_info : unit -> undo_info
 
-val init_undo : unit -> undo_cmds
+type reset_info = reset_status * undo_info * bool ref
 
+val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
 val reset_initial : unit -> unit
 val reset_to : reset_mark -> unit
 val reset_to_mod : identifier -> unit
@@ -65,6 +55,11 @@ val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit
 val interp_and_replace : string ->
       (reset_info * (Util.loc * Vernacexpr.vernac_expr)) * 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 *)
 
 type hyp = env * evar_map *
diff --git a/ide/coqide.ml b/ide/coqide.ml
index dc1e89cf1..734bdccdc 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -172,12 +172,12 @@ let cb = GData.clipboard Gdk.Atom.primary
 
 exception Size of int
 
-(* when pushing a segment end, all the previous sentences have their segment
- * boolean turned to false, causing backtrack to such sentences to be a
- * BackTrackToNextActiveMark *)
-let update_on_end_of_segment cmd_stk = let lookup_section item =
-  item.reset_info.segment <- false in try Stack.iter lookup_section cmd_stk with
-      Exit -> ()
+let update_on_end_of_segment cmd_stk id =
+  let lookup_section = function 
+    | { reset_info = ResetAtSegmentStart id',_,_ } when id = id' -> raise Exit
+    | { reset_info = _,_,r } -> r := false
+  in
+    try Stack.iter lookup_section cmd_stk with Exit -> ()
 
 let push_phrase cmd_stk reset_info start_of_phrase_mark end_of_phrase_mark ast =
   let x = {start = start_of_phrase_mark;
@@ -187,9 +187,9 @@ let push_phrase cmd_stk reset_info start_of_phrase_mark end_of_phrase_mark ast =
 	  } in
   begin
     match snd ast with
-    | VernacEndSegment _ ->
+    | VernacEndSegment (_,id) ->
         prerr_endline "Updating on end of segment 1";
-        update_on_end_of_segment cmd_stk
+        update_on_end_of_segment cmd_stk id
     | _ -> ()
   end;
   Stack.push x cmd_stk
@@ -199,59 +199,63 @@ let repush_phrase cmd_stk reset_info x =
   let x = { x with reset_info = reset_info } in
   begin
     match snd x.ast with
-      | VernacEndSegment _ ->
+      | VernacEndSegment (_,id) ->
           prerr_endline "Updating on end of segment 2";
-          update_on_end_of_segment cmd_stk
+          update_on_end_of_segment cmd_stk id
       | _ -> ()
   end;
   Stack.push x cmd_stk
 
-(* called ($ntacsteps - $prev_ntacsteps) times *)
-let add_undo x =
-  if x.p = 0 then { x with n = x.n + 1 } else x
-
-(* called $openproofs times *)
-let add_abort x =
-  if x.p = 0 then (*  *)
-    { x with n = 0; a = x.a + 1 }
-  else (* there was a closed proof between S+ and S0, and now there is an open proof between S0 and S- *)
-    { x with p = x.p - 1 }
-
-(* called at each update_proof call *)
-let add_qed q x =
-  if q = 0 then (* no closed proofs *)
-    x
-  else (* closed proofs *)
-    { x with b = BacktrackToNextActiveMark; p = x.p + q }
-
-let add_backtrack x b' =
-  { x with b = b' }
-
-let update_proofs x (prev_lems,prev_ntacsteps) =
-  let (cur_lems,ntacsteps) = x.l in
+type backtrack =
+| BacktrackToNextActiveMark
+| BacktrackToMark of reset_mark
+| BacktrackToModSec of Names.identifier
+| 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 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 =
   let ncommon = List.length (Util.list_intersect cur_lems prev_lems) in
   let openproofs = List.length cur_lems - ncommon in
   let closedproofs = List.length prev_lems - ncommon in
-  let undos = { x with l = (prev_lems,prev_ntacsteps) } in
-  let undos = add_qed closedproofs (Util.iterate add_abort openproofs undos) in
-  Util.iterate add_undo (ntacsteps - prev_ntacsteps) undos
+  let undos = (n,a,b,p,prev_lems) in
+  add_qed closedproofs (Util.iterate add_abort openproofs undos)
 
 let pop_command cmd_stk undos t =
-  let t = t.reset_info in
-  let (state_info,undo_info,section_info) = (t.state,(t.pending,t.pf_depth),t.segment) in
+  let (state_info,undo_info,section_info) = t.reset_info in
   let undos =
-    if section_info then (* segment ouvert, on saute directement au bon état *)
+    if !section_info then
       let undos = update_proofs undos undo_info in
-      add_backtrack undos (BacktrackToMark state_info)
-    else (* segment fermé, il faut sauter au debut du segment *)
+      match state_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
       begin
         prerr_endline "In section";
-        (* XXX - all the way to the bottom of the stack *)
-        add_backtrack undos BacktrackToNextActiveMark
+      (* An object inside a closed section *)
+      add_backtrack undos BacktrackToNextActiveMark
       end in
   ignore (Stack.pop cmd_stk);
   undos
 
+
+(* appelle Pfedit.delete_current_proof a fois
+ * utiliser Vernacentries.vernac_abort a la place ? *)
 let apply_aborts a =
   if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
   try Util.repeat a Pfedit.delete_current_proof ()
@@ -259,6 +263,8 @@ let apply_aborts a =
 
 exception UndoStackExhausted
 
+(* appelle Pfedit.undo n fois
+ * utiliser vernac_undo ? *)
 let apply_tactic_undo n =
   if n<>0 then
     (prerr_endline ("Applying "^string_of_int n^" undos");
@@ -267,20 +273,19 @@ let apply_tactic_undo n =
 
 let apply_reset = function
   | BacktrackToMark mark -> reset_to mark
+  | BacktrackToModSec id -> reset_to_mod id
   | NoBacktrack -> ()
   | BacktrackToNextActiveMark -> assert false
 
-(* XXX - in its current form, it goes all the way to the bottom of the stack. *)
-let rec apply_undos cmd_stk undos =
-  if undos.p = 0 & undos.b <> BacktrackToNextActiveMark then
-    (* pas de preuve fermée et dans un segment ouvert *)
+let rec apply_undos cmd_stk (n,a,b,p,l as undos) =
+  if p = 0 & b <> BacktrackToNextActiveMark then
     begin
-      apply_aborts undos.a;
+      apply_aborts a;
       try
-	apply_tactic_undo undos.n;
-	apply_reset undos.b
+	apply_tactic_undo n;
+	apply_reset b
       with UndoStackExhausted ->
-	apply_undos cmd_stk { undos with a = 0; b = BacktrackToNextActiveMark }
+	apply_undos cmd_stk (n,0,BacktrackToNextActiveMark,p,l)
     end
   else
     (* re-synchronize Coq to the current state of the stack *)
@@ -290,7 +295,7 @@ let rec apply_undos cmd_stk undos =
       begin
         let t = Stack.top cmd_stk in
         apply_undos cmd_stk (pop_command cmd_stk undos t);
-        let reset_info = Coq.compute_reset_info () in
+        let reset_info = Coq.compute_reset_info (snd t.ast) in
         interp_last t.ast;
         repush_phrase cmd_stk reset_info t
       end
@@ -1305,7 +1310,7 @@ object(self)
           else
             done_smthg, undos
     in
-    let undos = Coq.init_undo () in
+    let undos = (0,0,NoBacktrack,0,undo_info()) in
     let done_smthg, undos = pop_commands false undos in
       prerr_endline "Popped commands";
       if done_smthg then
@@ -1375,7 +1380,7 @@ object(self)
             self#show_goals;
             self#clear_message
           in
-          let undo = pop_command cmd_stack (Coq.init_undo ()) last_command in
+          let undo = pop_command cmd_stack (0,0,NoBacktrack,0,undo_info()) last_command in
             apply_undos cmd_stack undo;
             sync update_input ()
         with
@@ -1939,6 +1944,7 @@ let main files =
 		      input_buffer#place_cursor input_buffer#start_iter;
 		      prerr_endline ("Loading: switch to view "^ string_of_int index);
 		      session_notebook#goto_page index;
+		      prerr_endline "Loading: highlight";
 		      input_buffer#set_modified false;
 		      prerr_endline "Loading: clear undo";
 		      session.script#clear_undo;
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index ffb8c8d59..e92a345e3 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -107,3 +107,70 @@ let rec complete_forward w (it:GText.iter) =
 	    else Some (stop,stop,ne)
 	else complete_forward w stop
 
+
+let find_comment_end (start:GText.iter) =
+  let rec find_nested_comment (search_start:GText.iter) (search_end:GText.iter) (comment_end:GText.iter) =
+    match (search_start#forward_search ~limit:search_end "(*"),(comment_end#forward_search "*)") with
+      | None,_ -> comment_end
+      | Some _, None -> raise Not_found
+      | Some (_,next_search_start),Some (next_search_end,next_comment_end) ->
+          find_nested_comment next_search_start next_search_end next_comment_end
+  in
+    match start#forward_search "*)" with
+      | None -> raise Not_found
+      | Some (search_end,comment_end) -> find_nested_comment start search_end comment_end
+
+
+let rec find_string_end (start:GText.iter) =
+  let dblquote = int_of_char '"' in
+  let rec escaped_dblquote c =
+    (c#char = dblquote) && not (escaped_dblquote c#backward_char)
+  in
+    match start#forward_search "\"" with
+      | None -> raise Not_found
+      | Some (stop,next_start) ->
+          if escaped_dblquote stop#backward_char
+          then find_string_end next_start
+          else next_start
+
+
+let rec find_next_sentence (from:GText.iter) =
+  match (from#forward_search ".") with
+    | None -> raise Not_found
+    | Some (non_vernac_search_end,next_sentence) ->
+        match from#forward_search ~limit:non_vernac_search_end "(*",from#forward_search ~limit:non_vernac_search_end "\"" with
+          | None,None ->
+              if Glib.Unichar.isspace next_sentence#char || next_sentence#compare next_sentence#forward_char == 0
+              then next_sentence else find_next_sentence next_sentence
+          | None,Some (_,string_search_start) -> find_next_sentence (find_string_end string_search_start)
+          | Some (_,comment_search_start),None -> find_next_sentence (find_comment_end comment_search_start)
+          | Some (_,comment_search_start),Some (_,string_search_start) ->
+              find_next_sentence (
+                if comment_search_start#compare string_search_start < 0
+                then find_comment_end comment_search_start
+                else find_string_end string_search_start)
+
+
+let find_nearest_forward (cursor:GText.iter) targets =
+  let fold_targets acc target =
+    match cursor#forward_search target,acc with
+      | Some (t_start,_),Some nearest when (t_start#compare nearest < 0) -> Some t_start
+      | Some (t_start,_),None -> Some t_start
+      | _ -> acc
+  in
+    match List.fold_left fold_targets None targets with
+      | None -> raise Not_found
+      | Some nearest -> nearest
+
+
+let find_nearest_backward (cursor:GText.iter) targets =
+  let fold_targets acc target =
+    match cursor#backward_search target,acc with
+      | Some (t_start,_),Some nearest when (t_start#compare nearest > 0) -> Some t_start
+      | Some (t_start,_),None -> Some t_start
+      | _ -> acc
+  in
+    match List.fold_left fold_targets None targets with
+      | None -> raise Not_found
+      | Some nearest -> nearest
+