redirection of errors in coqide + dynamic warning printer (needed for tm_egg)

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

8 files changed, 33 insertions, 31 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 7893590abb..0c2e3905db 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -150,12 +150,14 @@ let set_highlight_timer f =
 (* Get back the standard coq out channels *)
 let read_stdout,clear_stdout =
   let out_buff = Buffer.create 100 in
-  Pp_control.std_ft := Format.formatter_of_buffer out_buff;
-  (fun () -> Format.pp_print_flush !Pp_control.std_ft (); 
+  let out_ft = Format.formatter_of_buffer out_buff in
+    Pp_control.std_ft := out_ft;
+    Pp_control.err_ft := out_ft;    
+  (fun () -> Format.pp_print_flush out_ft (); 
      let r = Buffer.contents out_buff in
      Buffer.clear out_buff; r),
   (fun () -> 
-     Format.pp_print_flush !Pp_control.std_ft (); Buffer.clear out_buff)
+     Format.pp_print_flush out_ft (); Buffer.clear out_buff)
 
 
 let last_dir = ref ""
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index d4e6eb722b..27ddae00c2 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -243,7 +243,7 @@ let pp_dirs ft =
 (* pretty print on stdout and stderr *)
 
 let pp_std_dirs = pp_dirs !std_ft
-let pp_err_dirs = pp_dirs err_ft
+let pp_err_dirs = pp_dirs !err_ft
 
 let ppcmds x = Ppdir_ppcmds x
 
@@ -265,12 +265,18 @@ let pp_with ft strm =
 let ppnl_with ft strm =
   pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >]
 
-let warning_with ft string =
-  ppnl_with ft [< warnstart() ; str "Warning: " ; str string ; warnend() >]
 
-let warn_with ft pps =
+let default_warn_with ft pps = 
   ppnl_with ft [< warnstart() ; str "Warning: " ; pps ; warnend() >]
 
+let pp_warn_with = ref default_warn_with
+
+let set_warning_function pp_warn = pp_warn_with := pp_warn
+
+let warn_with ft pps = !pp_warn_with ft pps 
+
+let warning_with ft string = warn_with ft (str string)
+
 let pp_flush_with ft =
   Format.pp_print_flush ft
 
@@ -288,19 +294,19 @@ let msg_warning_with ft strm=
 
 
 (* pretty printing functions WITHOUT FLUSH *)
-let pp        x = pp_with !std_ft x
+let pp        x = pp_with   !std_ft x
 let ppnl      x = ppnl_with !std_ft x
-let pperr     = pp_with err_ft
-let pperrnl   = ppnl_with err_ft
-let message s = ppnl (str s)
-let warning   x = warning_with err_ft x
-let warn      x = warn_with err_ft x
+let pperr     x = pp_with   !err_ft x
+let pperrnl   x = ppnl_with !err_ft x
+let message   s = ppnl      (str s)
+let warning   x = warning_with !err_ft x
+let warn      x = warn_with    !err_ft x
 let pp_flush  x = Format.pp_print_flush !std_ft x
 let flush_all() = flush stderr; flush stdout; pp_flush()
 
 (* pretty printing functions WITH FLUSH *)
 let msg x = msg_with !std_ft x
 let msgnl x = msgnl_with !std_ft x
-let msgerr = msg_with err_ft
-let msgerrnl = msgnl_with err_ft
-let msg_warning x = msg_warning_with err_ft x
+let msgerr x = msg_with !err_ft x
+let msgerrnl x = msgnl_with !err_ft x
+let msg_warning x = msg_warning_with !err_ft x
diff --git a/lib/pp.mli b/lib/pp.mli
index 7b9d7d6637..a0177d7410 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -80,6 +80,8 @@ val warning_with : Format.formatter -> string -> unit
 val warn_with : Format.formatter -> std_ppcmds -> unit
 val pp_flush_with : Format.formatter -> unit -> unit
 
+val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit 
+
 (*s Pretty-printing functions \emph{with flush}. *)
 
 val msg_with : Format.formatter -> std_ppcmds -> unit
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 0b886342d8..e439161251 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -89,7 +89,8 @@ let with_output_to ch =
 let std_ft = ref Format.std_formatter
 let _ = set_dflt_gp !std_ft
 
-let err_ft = with_output_to stderr
+let err_ft = ref Format.err_formatter
+let _ = set_gp !err_ft deep_gp
 
 let deep_ft = with_output_to stdout
 let _ = set_gp deep_ft deep_gp
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 24faf96f4d..3c008aaca1 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -37,7 +37,7 @@ val with_fp : 'a pp_formatter_params -> Format.formatter
 val with_output_to : out_channel -> Format.formatter
 
 val std_ft : Format.formatter ref
-val err_ft : Format.formatter
+val err_ft : Format.formatter ref
 val deep_ft : Format.formatter
 
 (*s For parametrization through vernacular. *)
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 442bbb6aff..7e32879d2a 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -64,7 +64,7 @@ let rec extract_signature = function
 let check_unicity s l =
   let l' = List.map (fun (l,_) -> extract_signature l) l in
   if not (Util.list_distinct l') then
-    Pp.warning_with Pp_control.err_ft
+    Pp.warning_with !Pp_control.err_ft
       ("Two distinct rules of tactic entry "^s^" have the same\n"^
       "non-terminals in the same order: put them in distinct tactic entries")
 
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 22df73ba73..5e8337fe97 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -56,7 +56,7 @@ let rec extract_signature = function
 let check_unicity s l =
   let l' = List.map (fun (_,l,_) -> extract_signature l) l in
   if not (Util.list_distinct l') then
-    Pp.warning_with Pp_control.err_ft
+    Pp.warning_with !Pp_control.err_ft
       ("Two distinct rules of entry "^s^" have the same\n"^
       "non-terminals in the same order: put them in distinct vernac entries")
 
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 8a22e8b8d9..e4fa9cc9ef 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -290,7 +290,7 @@ let justification tac gls=
 	   error "insufficient justification" 
 	 else
 	   begin
-	     msgnl (str "Warning: insufficient justification");  
+	     msg_warning (str "insufficient justification");  
 	     daimon_tac gls
 	   end) gls
 
@@ -424,8 +424,6 @@ let thus_tac c ctyp submetas gls =
       error "I could not relate this statement to the thesis" in
   let nflist = nf_list evd list in
   let nfgoal = nf_meta evd info.pm_partial_goal in
-(*  let _ = msgnl (str "Partial goal : " ++ 
-		   print_constr_env (pf_env gls) nfgoal) in *)
   let rgl = ref None in
   let refiner = max_linear_context rgl nfgoal in
     match !rgl with
@@ -1263,13 +1261,6 @@ match id in t return p with
 end*)
 
 
-    
-
-
-
-
-
-
 let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = 
   match tree with
       Pop t ->  
@@ -1321,7 +1312,7 @@ let rec execute_cases at_top fix_name per_info kont0 stacks tree gls =
 		push_head (constr i) is_rec ids br_stacks in
 		execute_cases false fix_name per_info kont0 p_stacks tree 
 	  | None -> 
-	      msgnl (str "Warning : missing case");
+	      msg_warning (str "missing case");
 	      kont0 (mkMeta 1) 
 	in
 	let id = pf_get_new_id patvar_base gls in