Amélioration de la colorisation, du backtrack et des messages de CoqIDE

- Colorisation:
  - on ne colorie que les noms de commandes que si en début de phrase
    (par exemple: Definition F := fun Local => Local) ne colorie pas
    Local),
  - ajout de motifs plus sophistiqué, (par exemple, tous les Set/Unset
    sont uniformément mis en valeur).
- Backtracking: résolution bug #1538 et réactivation de la possibilité de
  déclarer des défs, types, etc pendant une session de preuve. En revanche,
  il n'est pas clair que cela fonctionne bien avec le mode déclaratif.
- Messages d'erreur : on ne capture la sortie de coq qu'après
  l'initialisation pour que les erreurs d'initialisation soit
  affichées (cf bug #1424 and item 5 of #1123).



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

1 files changed, 37 insertions, 21 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 29b55da6a..1e6892d0d 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -159,7 +159,7 @@ object('self)
   method activate : unit -> unit
   method active_keypress_handler : GdkEvent.Key.t -> bool
   method backtrack_to : GText.iter -> unit
-  method backtrack_to_no_lock : GText.iter -> unit
+  method backtrack_to_no_lock : GText.iter -> Names.identifier list -> unit
   method clear_message : unit
   method deactivate : unit -> unit
   method disconnected_keypress_handler : GdkEvent.Key.t -> bool
@@ -1271,22 +1271,34 @@ object(self)
 	    self#clear_message)();
     Coq.reset_initial ()
 
-
   (* backtrack Coq to the phrase preceding iterator [i] *)
-  method backtrack_to_no_lock i =
+  method backtrack_to_no_lock i oldest_id_to_reset =
     prerr_endline "Backtracking_to iter starts now.";
+    let was_refining = Pfedit.refining () in
     (* re-synchronize Coq to the current state of the stack *)
-    let rec synchro () =
+    let rec synchro oldest_decl_in_middle_of_proof =
       if is_empty () then
 	Coq.reset_initial ()
       else begin
 	  let t = pop () in
 	    begin match t.reset_info with
-	      | ResetAtSegmentStart (id, ({contents=true} as v)) ->
-		  v:=false; reset_to_mod id
-	      | ResetAtDecl (id, ({contents=true} as v)) ->
-		  v:=false; reset_to id
-	      | _ -> synchro ()
+	      | ResetAtSegmentStart (id, {contents=true}) ->
+		  reset_to_mod id
+	      | ResetAtDecl (id, {contents=true}) ->
+		  if was_refining then
+		    (prerr_endline ("Skipping "^Names.string_of_id id);
+		    synchro [id])
+		  else
+		    reset_to (List.hd (oldest_decl_in_middle_of_proof@[id]))
+	      | ResetAtDecl (id, {contents=false}) ->
+		  if was_refining then
+		    (*reset oldest decl found before theorem started, if any*)
+		    List.iter reset_to oldest_decl_in_middle_of_proof
+		  else
+		    (prerr_endline ("Skipping "^Names.string_of_id id);
+		    synchro [id])
+	      | _ ->
+		  synchro oldest_decl_in_middle_of_proof
 	    end;
 	    interp_last t.ast;
 	    repush_phrase t
@@ -1301,9 +1313,12 @@ object(self)
       else
 	let t = top () in 
 	  if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then begin
+	    prerr_endline "Popped top command";
 	      ignore (pop ());
-	      let undos = if is_tactic (snd t.ast) then add_undo undos else None in
-		pop_commands true undos
+	      let undos =
+		if is_vernac_tactic_command (snd t.ast) then add_undo undos
+		else None in
+	      pop_commands true undos
 	    end else
 	    done_smthg, undos
     in
@@ -1313,8 +1328,8 @@ object(self)
 	begin 
 	  try 
 	    (match undos with 
-	       | None -> synchro () 
-	       | Some n -> try Pfedit.undo n with _ -> synchro ());
+	       | None -> synchro oldest_id_to_reset
+	       | Some n -> try Pfedit.undo n with _ -> synchro oldest_id_to_reset);
             sync (fun _ ->
 		    let start =
 		      if is_empty () then input_buffer#start_iter 
@@ -1342,7 +1357,8 @@ Please restart and report NOW.";
       
   method backtrack_to i = 
     if Mutex.try_lock coq_may_stop then 
-      (!push_info "Undoing...";self#backtrack_to_no_lock i ; Mutex.unlock coq_may_stop;
+      (!push_info "Undoing...";
+       self#backtrack_to_no_lock i []; Mutex.unlock coq_may_stop;
        !pop_info ())
     else prerr_endline "backtrack_to : discarded (lock is busy)"
 
@@ -1381,7 +1397,7 @@ Please restart and report NOW.";
 		| {ast=_, (VernacSolve _ | VernacTime (VernacSolve _))} -> 
 		    begin 
 		      try Pfedit.undo 1; ignore (pop ()); sync update_input () 
-		      with _ -> self#backtrack_to_no_lock start
+		      with _ -> self#backtrack_to_no_lock start []
 		    end
 
 		| {reset_info=ResetAtSegmentStart (id, {contents=true})} ->
@@ -1389,9 +1405,10 @@ Please restart and report NOW.";
 		    reset_to_mod id;
 		    sync update_input ()
 		| {reset_info=ResetAtDecl (id, {contents=true})} ->
-		    ignore (pop ());
-		    reset_to id;
-		    sync update_input ()
+		    if Pfedit.refining () then
+		      self#backtrack_to_no_lock start [id]
+		    else
+		      (ignore (pop ()); sync update_input ())
 		| {reset_info=ResetAtDecl (id,{contents=false})} ->
 		    ignore (pop ());
 		    (try 
@@ -1406,7 +1423,7 @@ Please restart and report NOW.";
 		    ignore (pop ());
 		    sync update_input ()
 		| _ -> 
-		    self#backtrack_to_no_lock start
+		    self#backtrack_to_no_lock start []
 	      end;
 	with
 	  | Size 0 -> (* !flash_info "Nothing to Undo"*)()
@@ -3468,6 +3485,7 @@ let start () =
 		  else failwith ("Coqide internal error: " ^ msg)));
     Command_windows.main ();
     Blaster_window.main 9;
+    init_stdout ();
     main files;
     if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ()); 
     while true do 
@@ -3480,5 +3498,3 @@ let start () =
 	    flush stderr;
 	    crash_save 127
     done
-      
-