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

4 files changed, 24 insertions, 15 deletions

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. *)