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

7 files changed, 135 insertions, 91 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index aef993be65..41a6abad44 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -112,7 +112,7 @@ let user_error_loc l s =
 
 type command_attribute =
     NavigationCommand | QueryCommand | DebugCommand
-  | OtherStatePreservingCommand | GoalStartingCommand
+  | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand
 
 let rec attribute_of_vernac_command = function
   (* Control *)
@@ -167,8 +167,8 @@ let rec attribute_of_vernac_command = function
   | VernacDeclareInstance _ -> []
 
   (* Solving *)
-  | VernacSolve _ -> []
-  | VernacSolveExistential _ -> []
+  | VernacSolve _ -> [SolveCommand]
+  | VernacSolveExistential _ -> [SolveCommand]
 
   (* MMode *)
   | VernacDeclProof -> []
@@ -243,6 +243,7 @@ let rec attribute_of_vernac_command = function
   | VernacToplevelControl _ -> []
 
   (* Extensions *)
+  | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
   | VernacExtend _ -> []
 
 let is_vernac_goal_starting_command com =
@@ -257,18 +258,18 @@ let is_vernac_query_command com =
 let is_vernac_debug_command com =
   List.mem DebugCommand (attribute_of_vernac_command com)
 
+let is_vernac_goal_printing_command com =
+  let attribute = attribute_of_vernac_command com in
+  List.mem GoalStartingCommand attribute or
+  List.mem SolveCommand attribute
+
 let is_vernac_state_preserving_command com =
   let attribute = attribute_of_vernac_command com in
-  let b =
-    List.mem OtherStatePreservingCommand attribute or
-    List.mem QueryCommand attribute in
-  if b then prerr_endline "state preserving command found";
-  b
-
-let rec is_tactic = function
-  | VernacSolve _ -> true
-  | VernacTime com -> is_tactic com
-  | _ -> false
+  List.mem OtherStatePreservingCommand attribute or
+  List.mem QueryCommand attribute
+
+let is_vernac_tactic_command com =
+  List.mem SolveCommand (attribute_of_vernac_command com)
 
 let interp verbosely s = 
   prerr_endline "Starting interp...";
@@ -287,7 +288,9 @@ let interp verbosely s =
 	if is_vernac_query_command vernac then 
 	  !flash_info
 	    "Warning: query commands should not be inserted in scripts";
-	Flags.make_silent (not verbosely); (*verbose if in small step forward*)
+	if not (is_vernac_goal_printing_command vernac) then
+	  (* Verbose if in small step forward and not a tactic *)
+	  Flags.make_silent (not verbosely);
 	Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s));
 	Flags.make_silent true;
 	prerr_endline ("...Done with interp of : "^s);
diff --git a/ide/coq.mli b/ide/coq.mli
index 32a62c2306..9c8e273200 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -20,7 +20,7 @@ val interp : bool -> string -> Util.loc * Vernacexpr.vernac_expr
 val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit
 val interp_and_replace : string -> (Util.loc * Vernacexpr.vernac_expr) * string
 
-val is_tactic : Vernacexpr.vernac_expr -> bool
+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
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 29b55da6aa..1e6892d0d6 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
-      
-      
diff --git a/ide/highlight.mll b/ide/highlight.mll
index 79b4e25aa7..6649dc31a7 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -18,18 +18,15 @@
 
   let comment_start = ref 0
 
-  let is_keyword =
+  (* Without this table, the automaton would be too big and
+     ocamllex would fail *)
+  let is_one_word_command =
     let h = Hashtbl.create 97 in
     List.iter (fun s -> Hashtbl.add h s ())
-      [  "Add" ; "Check"; "Defined" ; 
-	 "End" ; "Eval"; "Export" ; "Extraction" ; "Hint" ; "Hints" ;
-	 "Implicits" ; "Import" ; 
-	 "Infix" ; "Load" ; "Module" ;
-	 "Notation"; "Proof" ; "Print"; "Qed" ;
-	 "Require" ; "Reset"; "Undo"; "Save" ;
-	 "Section" ; "Unset" ;
-	 "Set" ; "Notation";
-	 "Implicit"; "Arguments"; "Unfold"; "Resolve"
+      [  "Add" ; "Check"; "Eval"; "Extraction" ;
+	 "Load" ; "Undo";
+	 "Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ;
+	 "End" ; "Section"
       ];
     Hashtbl.mem h
 
@@ -38,20 +35,31 @@
       List.iter (fun s -> Hashtbl.add h s ())
 	[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for"; 
 	  "end"; "as"; "let"; "in"; "dest"; "if"; "then"; "else"; "return";
-	  "Prop"; "Set"; "Type"]; 
+	  "Prop"; "Set"; "Type" ]; 
       Hashtbl.mem h
 
-  let is_declaration =
+  (* Without this table, the automaton would be too big and
+     ocamllex would fail *)
+  let is_one_word_declaration =
     let h = Hashtbl.create 97 in
       List.iter (fun s -> Hashtbl.add h s ())
-	[ "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ; "Proposition" ; "Property" ;
-	  "Definition" ; "Let" ; "Example" ; "SubClass" ; "Inductive" ; "CoInductive" ; 
-	  "Record" ; "Structure" ; "Fixpoint" ; "CoFixpoint"; 
+	[ (* Theorems *)
+          "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ;
+	  "Proposition" ; "Property" ;
+          (* Definitions *)
+	  "Definition" ; "Let" ; "Example" ; "SubClass" ;
+          "Fixpoint" ; "CoFixpoint"; 
+          (* Assumptions *)
 	  "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ;
-	  "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters"
+	  "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters";
+          (* Inductive *)
+          "Inductive" ; "CoInductive" ; "Record" ; "Structure" ;
+          (* Other *)
+	  "Ltac" ; "Typeclasses"; "Instance"
 	];
       Hashtbl.mem h
 
+  let starting = ref true
 }
 
 let space = 
@@ -62,44 +70,54 @@ let identchar =
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
 let ident = firstchar identchar*
 
-let thm_token = "Theorem" | "Lemma" | "Fact" | "Remark" | "Corollary" | "Proposition" | "Property"
-
-let def_token = "Definition" | "Let" | "Example" | "SubClass"
-
-let assumption = "Hypothesis" | "Variable" | "Axiom" | "Parameter" | "Conjecture" |
-  "Hypotheses" | "Variables" | "Axioms" | "Parameters"
-
-let declaration = 
-  "Theorem" | "Lemma" | "Fact" | "Remark" | "Corollary" | "Proposition" | "Property" |
-  "Definition" | "Let" | "Example" | "SubClass" |
-  "Inductive" | "CoInductive" | 
-  "Record" | "Structure" |
-  "Fixpoint" | "CoFixpoint"
-       
+let multiword_declaration =
+  "Module" (space+ "Type")
+| "Program" space+ ident
+
+let locality = ("Local" space+)?
+
+let multiword_command =
+  "Set" (space+ ident)* 
+| "Unset" (space+ ident)* 
+| "Open" space+ locality "Scope"
+| "Next" space+ "Obligation"
+| "Solve" space+ "Obligations"
+| "Require" space+ ("Import"|"Export")
+| "Infix" space+ locality
+| "Notation" space+ locality
+| "Hint" space+ locality ident
+| "Reset" (space+ "Initial")?
+| "Tactic" space+ "Notation"
+
+rule next_starting_order = parse
+  | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf }
+  | space+ { next_starting_order lexbuf }
+  | multiword_declaration
+      { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, "decl" }
+  | multiword_command
+      { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, "kwd" }
+  | ident as id 
+      { starting:=false; 
+        if is_one_word_command id then 
+	  lexeme_start lexbuf, lexeme_end lexbuf, "kwd" 
+	else if is_one_word_declaration id then
+	  lexeme_start lexbuf, lexeme_end lexbuf, "decl"
+	else
+	  next_interior_order lexbuf
+      }
+  | _    { starting := false; next_interior_order lexbuf}
+  | eof  { raise End_of_file }
 
-rule next_order = parse
+and next_interior_order = parse
   | "(*" 
       { comment_start := lexeme_start lexbuf; comment lexbuf }
-  | "Module Type"
-      { lexeme_start lexbuf, lexeme_end lexbuf, "kwd" }
-  | "Program" space+ ident { lexeme_start lexbuf, lexeme_end lexbuf, "decl" }
   | ident as id 
-      { if is_keyword id then 
-	    lexeme_start lexbuf, lexeme_end lexbuf, "kwd" 
-	else 
-	    begin
-	      if is_constr_kw id then
-		lexeme_start lexbuf, lexeme_end lexbuf, "kwd"
-	      else
-		begin
-		  if is_declaration id then
-		    lexeme_start lexbuf, lexeme_end lexbuf, "decl"
-		  else
-		    next_order lexbuf 
-		end
-	    end
-      }
-  | _    { next_order lexbuf}
+      { if is_constr_kw id then
+	  lexeme_start lexbuf, lexeme_end lexbuf, "kwd"
+        else
+	  next_interior_order lexbuf }
+  | "." (" "|"\n"|"\t") { starting := true; next_starting_order lexbuf }
+  | _    { next_interior_order lexbuf}
   | eof  { raise End_of_file }
 
 and comment = parse
@@ -114,6 +132,7 @@ and comment = parse
   let highlighting = ref false
 
   let highlight_slice (input_buffer:GText.buffer) (start:GText.iter) stop = 
+    starting := true; (* approximation: assume the beginning of a sentence *)
     if !highlighting then prerr_endline "Rejected highlight" 
     else begin
       highlighting := true;
@@ -130,7 +149,10 @@ and comment = parse
 	let lb = Lexing.from_string s in
 	try 
 	  while true do
-	    let b,e,o=next_order lb in
+	    let b,e,o =
+	      if !starting then next_starting_order lb
+	      else next_interior_order lb in
+	    
 	    let b,e = convert_pos b,convert_pos e in
 	    let start = input_buffer#get_iter_at_char (offset + b) in
 	    let stop = input_buffer#get_iter_at_char (offset + e) in
@@ -142,7 +164,7 @@ and comment = parse
       highlighting := false
     end
 
-  let highlight_current_line input_buffer = 
+  let highlight_current_line input_buffer =
     try 
       let i = get_insert input_buffer in
       highlight_slice input_buffer (i#set_line_offset 0) i
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index f4fd73d6fd..a3fd090840 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -148,13 +148,15 @@ let set_highlight_timer f =
 
 
 (* Get back the standard coq out channels *)
-let read_stdout,clear_stdout =
+let init_stdout,read_stdout,clear_stdout =
   let out_buff = Buffer.create 100 in
   let out_ft = Format.formatter_of_buffer out_buff in
+  (fun () -> 
     Pp_control.std_ft := out_ft;
-    Pp_control.err_ft := out_ft;    
+    Pp_control.err_ft := out_ft),
   (fun () -> Format.pp_print_flush out_ft (); 
      let r = Buffer.contents out_buff in
+     prerr_endline "Output from Coq is: "; prerr_endline r;
      Buffer.clear out_buff; r),
   (fun () -> 
      Format.pp_print_flush out_ft (); Buffer.clear out_buff)
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 5dad5b18b1..6b8307fc59 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -17,6 +17,7 @@ val mutex : string -> ('a -> unit) -> 'a -> unit
 val browse : (string -> unit) -> string -> unit
 val browse_keyword : (string -> unit) -> string -> unit
 val byte_offset_to_char_offset : string -> int -> int
+val init_stdout : unit -> unit
 val clear_stdout : unit -> unit
 val debug : bool ref
 val disconnect_revert_timer : unit -> unit
diff --git a/ide/preferences.ml b/ide/preferences.ml
index aeaeb4ec17..daca874add 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -276,7 +276,7 @@ let load_pref () =
     set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v);
     current := np;
 (*
-    Format.printf "in laod_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
+    Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
 *)
   with e -> 
     prerr_endline ("Could not load preferences ("^