Refactoring of coqide backtrack code, with the intent to put everything

into coqtop.

Also, some cleaning in ide/gtk_parsing.ml.

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

4 files changed, 100 insertions, 158 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index bf1140552..6018cc07e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -340,21 +340,41 @@ let is_vernac_goal_printing_command com =
   List.mem GoalStartingCommand attribute or
   List.mem SolveCommand attribute
 
-type undo_info = identifier list * int
-
-let undo_info () = Pfedit.get_all_proof_names (), Pfedit.current_proof_depth()
-
 type reset_mark = Libnames.object_name
 
-type reset_info = reset_mark * undo_info * bool ref
+type reset_info = {
+  state : reset_mark;
+  pending : identifier list;
+  pf_depth : int;
+  mutable segment : bool;
+}
 
 let compute_reset_info () =
-  (match Lib.has_top_frozen_state () with
+  match Lib.has_top_frozen_state () with
     | Some st ->
-	prerr_endline ("On top of state "^Libnames.string_of_path (fst st));
-	st
+        { state = st;
+          pending = Pfedit.get_all_proof_names ();
+          pf_depth = Pfedit.current_proof_depth ();
+          segment = true; }
     | None ->
-	failwith "FATAL ERROR: NO RESET"), undo_info(), ref true
+        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 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_initial () =
   prerr_endline "Reset initial called"; flush stderr;
@@ -410,41 +430,6 @@ 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 c2f96a1fe..a03528f81 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -31,13 +31,30 @@ val printing_state : printing_state
 
 type reset_mark
 
-type undo_info = identifier list * int
+type reset_info = {
+  state : reset_mark;
+  pending : identifier list;
+  pf_depth : int;
+  mutable segment : bool;
+}
 
-val undo_info : unit -> undo_info
+val compute_reset_info : unit -> reset_info
 
-type reset_info = reset_mark * undo_info * bool ref
+type backtrack =
+  | BacktrackToNextActiveMark
+  | BacktrackToMark of reset_mark
+  | NoBacktrack
+
+type undo_cmds = {
+  n : int;
+  a : int;
+  b : backtrack;
+  p : int;
+  l : (identifier list * int);
+}
+
+val init_undo : unit -> undo_cmds
 
-val compute_reset_info : unit -> reset_info
 val reset_initial : unit -> unit
 val reset_to : reset_mark -> unit
 val reset_to_mod : identifier -> unit
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 90673b67f..a22e4b4df 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -175,11 +175,12 @@ let cb = GData.clipboard Gdk.Atom.primary
 
 exception Size of int
 
-let update_on_end_of_segment cmd_stk id =
-  let lookup_section = function
-    | { reset_info = _,_,r } -> r := false
-  in
-    try Stack.iter lookup_section cmd_stk with Exit -> ()
+(* 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 push_phrase cmd_stk reset_info start_of_phrase_mark end_of_phrase_mark ast =
   let x = {start = start_of_phrase_mark;
@@ -189,9 +190,9 @@ let push_phrase cmd_stk reset_info start_of_phrase_mark end_of_phrase_mark ast =
 	  } in
   begin
     match snd ast with
-    | VernacEndSegment (_,id) ->
+    | VernacEndSegment _ ->
         prerr_endline "Updating on end of segment 1";
-        update_on_end_of_segment cmd_stk id
+        update_on_end_of_segment cmd_stk
     | _ -> ()
   end;
   Stack.push x cmd_stk
@@ -201,52 +202,59 @@ let repush_phrase cmd_stk reset_info x =
   let x = { x with reset_info = reset_info } in
   begin
     match snd x.ast with
-      | VernacEndSegment (_,id) ->
+      | VernacEndSegment _ ->
           prerr_endline "Updating on end of segment 2";
-          update_on_end_of_segment cmd_stk id
+          update_on_end_of_segment cmd_stk
       | _ -> ()
   end;
   Stack.push x cmd_stk
 
-type backtrack =
-| BacktrackToNextActiveMark
-| BacktrackToMark of reset_mark
-| 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,ntacsteps)) (prev_lems,prev_ntacsteps) =
+(* 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
   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 = (n,a,b,p,(prev_lems,prev_ntacsteps)) 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 pop_command cmd_stk undos t =
-  let (state_info,undo_info,section_info) = t.reset_info in
+  let t = t.reset_info in
+  let (state_info,undo_info,section_info) = (t.state,(t.pending,t.pf_depth),t.segment) in
   let undos =
-    if !section_info then
+    if section_info then (* segment ouvert, on saute directement au bon état *)
       let undos = update_proofs undos undo_info in
       add_backtrack undos (BacktrackToMark state_info)
-    else
+    else (* segment fermé, il faut sauter au debut du segment *)
       begin
         prerr_endline "In section";
-      (* An object inside a closed section *)
-      add_backtrack undos BacktrackToNextActiveMark
+        (* XXX - all the way to the bottom of the stack *)
+        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 ()
@@ -254,8 +262,6 @@ 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,15 +273,17 @@ let apply_reset = function
   | NoBacktrack -> ()
   | BacktrackToNextActiveMark -> assert false
 
-let rec apply_undos cmd_stk (n,a,b,p,l as undos) =
-  if p = 0 & b <> BacktrackToNextActiveMark then
+(* 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 *)
     begin
-      apply_aborts a;
+      apply_aborts undos.a;
       try
-	apply_tactic_undo n;
-	apply_reset b
+	apply_tactic_undo undos.n;
+	apply_reset undos.b
       with UndoStackExhausted ->
-	apply_undos cmd_stk (n,0,BacktrackToNextActiveMark,p,l)
+	apply_undos cmd_stk { undos with a = 0; b = BacktrackToNextActiveMark }
     end
   else
     (* re-synchronize Coq to the current state of the stack *)
@@ -1274,7 +1282,7 @@ object(self)
           else
             done_smthg, undos
     in
-    let undos = (0,0,NoBacktrack,0,undo_info()) in
+    let undos = Coq.init_undo () in
     let done_smthg, undos = pop_commands false undos in
       prerr_endline "Popped commands";
       if done_smthg then
@@ -1344,7 +1352,7 @@ object(self)
             self#show_goals;
             self#clear_message
           in
-          let undo = pop_command cmd_stack (0,0,NoBacktrack,0,undo_info()) last_command in
+          let undo = pop_command cmd_stack (Coq.init_undo ()) last_command in
             apply_undos cmd_stack undo;
             sync update_input ()
         with
@@ -1909,7 +1917,6 @@ 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 e92a345e3..ffb8c8d59 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -107,70 +107,3 @@ 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
-