This patch splits pretty printing representation from IO operations.

10 files changed, 260 insertions, 329 deletions

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index f7bd81f85d..d06d4b3768 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -88,7 +88,7 @@ let load_aux_file_for vfile =
   | Sys_error s | Scanf.Scan_failure s
   | Failure s | Invalid_argument s ->
      Flags.if_verbose
-       Pp.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s);
+       Feedback.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s);
      empty_aux_file
 
 let set h loc k v = set h (Loc.unloc loc) k v
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 3c1c5da33c..c3ec4a696e 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -28,13 +28,14 @@ CArray
 CStack
 Util
 Stateid
-Feedback
 Pp
 Ppstyle
+Xml_datatype
+Richpp
+Feedback
 Xml_lexer
 Xml_parser
 Xml_printer
-Richpp
 CUnix
 Envars
 Aux_file
diff --git a/lib/explore.ml b/lib/explore.ml
index 587db11563..aa7bddf2b4 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -27,7 +27,7 @@ module Make = functor(S : SearchProblem) -> struct
       | [i] -> int i
       | i :: l -> pp_rec l ++ str "." ++ int i
     in
-    msg_debug (h 0 (pp_rec p) ++ pp)
+    Feedback.msg_debug (h 0 (pp_rec p) ++ pp)
 
   (*s Depth first search. *)
 
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 1a90685de6..dce4372ec0 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -9,7 +9,7 @@
 open Xml_datatype
 open Serialize
 
-type message_level =
+type level =
   | Debug of string
   | Info
   | Notice
@@ -17,7 +17,7 @@ type message_level =
   | Error
 
 type message = {
-  message_level : message_level;
+  message_level : level;
   message_content : xml;
 }
 
@@ -169,3 +169,129 @@ let is_feedback = function
   | _ -> false
 
 let default_route = 0
+
+(** Feedback and logging *)
+open Pp
+open Pp_control
+
+type logger = level -> std_ppcmds -> unit
+
+let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ())
+let msgnl          strm = msgnl_with !std_ft strm
+
+(* XXX: This is really painful! *)
+module Emacs = struct
+
+  (* Special chars for emacs, to detect warnings inside goal output *)
+  let emacs_quote_start = String.make 1 (Char.chr 254)
+  let emacs_quote_end   = String.make 1 (Char.chr 255)
+
+  let emacs_quote_err g =
+    hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
+
+  let emacs_quote_info_start = "<infomsg>"
+  let emacs_quote_info_end = "</infomsg>"
+
+  let emacs_quote_info g =
+    hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
+
+end
+
+open Emacs
+
+let  dbg_str = str "Debug:"   ++ spc ()
+let info_str = mt ()
+let warn_str = str "Warning:" ++ spc ()
+let  err_str = str "Error:"   ++ spc ()
+
+let make_body quoter info s = quoter (hov 0 (info ++ s))
+
+(* Generic logger *)
+let gen_logger dbg err level msg = match level with
+  | Debug _ -> msgnl (make_body dbg  dbg_str msg)
+  | Info    -> msgnl (make_body dbg info_str msg)
+  | Notice  -> msgnl msg
+  | Warning -> Flags.if_warn (fun () ->
+               msgnl_with !err_ft (make_body err warn_str msg)) ()
+  | Error   -> msgnl_with !err_ft (make_body err  err_str msg)
+
+(** Standard loggers *)
+let std_logger   = gen_logger (fun x -> x) (fun x -> x)
+
+(* Color logger *)
+let color_terminal_logger level strm =
+  let msg = Ppstyle.color_msg in
+  match level with
+  | Debug _ -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
+  | Info    -> msg !std_ft strm
+  | Notice  -> msg !std_ft strm
+  | Warning ->
+    let header = ("Warning", Ppstyle.warning_tag) in
+    Flags.if_warn (fun () -> msg ~header !err_ft strm) ()
+  | Error -> msg ~header:("Error", Ppstyle.error_tag) !err_ft strm
+
+(* Rules for emacs:
+   - Debug/info: emacs_quote_info
+   - Warning/Error: emacs_quote_err
+   - Notice: unquoted
+ *)
+let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
+
+let logger       = ref std_logger
+let set_logger l = logger := l
+
+let msg_info    x = !logger Info x
+let msg_notice  x = !logger Notice x
+let msg_warning x = !logger Warning x
+let msg_error   x = !logger Error x
+let msg_debug   x = !logger (Debug "_") x
+
+(** Feeders *)
+let feeder = ref ignore
+let set_feeder f = feeder := f
+
+let feedback_id    = ref (Edit 0)
+let feedback_route = ref default_route
+
+let set_id_for_feedback ?(route=default_route) i =
+  feedback_id := i; feedback_route := route
+
+let feedback ?id ?route what =
+  !feeder {
+     contents = what;
+     route = Option.default !feedback_route route;
+     id    = Option.default !feedback_id id;
+  }
+
+let feedback_logger lvl msg =
+  feedback ~route:!feedback_route ~id:!feedback_id (
+    Message {
+      message_level   = lvl;
+      message_content = Richpp.of_richpp (Richpp.richpp_of_pp msg);
+    })
+
+(* Output to file *)
+let ft_logger old_logger ft level mesg =
+  let id x = x in
+  match level with
+  | Debug _ -> msgnl_with ft (make_body id  dbg_str mesg)
+  | Info    -> msgnl_with ft (make_body id info_str mesg)
+  | Notice  -> msgnl_with ft mesg
+  | Warning -> old_logger level mesg
+  | Error   -> old_logger level mesg
+
+let with_output_to_file fname func input =
+  let old_logger = !logger in
+  let channel = open_out (String.concat "." [fname; "out"]) in
+  logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
+  try
+    let output = func input in
+    logger := old_logger;
+    close_out channel;
+    output
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    logger := old_logger;
+    close_out channel;
+    Exninfo.iraise reraise
+
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 0d8e20230d..1e96f9a497 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -9,7 +9,7 @@
 open Xml_datatype
 
 (* Old plain messages (used to be in Pp) *)
-type message_level =
+type level =
   | Debug of string
   | Info
   | Notice
@@ -17,7 +17,7 @@ type message_level =
   | Error
 
 type message = {
-  message_level : message_level;
+  message_level : level;
   message_content : xml;
 }
 
@@ -66,3 +66,80 @@ val of_feedback : feedback -> xml
 val to_feedback : xml -> feedback
 val is_feedback : xml -> bool
 
+(** {6 Feedback sent, even asynchronously, to the user interface} *)
+
+(** Moved here from pp.ml *)
+
+(* Morally the parser gets a string and an edit_id, and gives back an AST.
+ * Feedbacks during the parsing phase are attached to this edit_id.
+ * The interpreter assignes an exec_id to the ast, and feedbacks happening
+ * during interpretation are attached to the exec_id.
+ * Only one among state_id and edit_id can be provided. *)
+
+(** A [logger] takes a level plus a pretty printing doc and logs it *)
+type logger = level -> Pp.std_ppcmds -> unit
+
+(** [set_logger l] makes the [msg_*] to use [l] for logging *)
+val set_logger : logger -> unit
+
+(** [std_logger] standard logger to [stdout/stderr]  *)
+val std_logger : logger
+
+val color_terminal_logger : logger
+(* This logger will apply the proper {!Pp_style} tags, and in
+   particular use the formatters {!Pp_control.std_ft} and
+   {!Pp_control.err_ft} to display those messages. Be careful this is
+   not compatible with the Emacs mode!  *)
+
+(** [feedback_logger] will produce feedback messages instead IO events *)
+val feedback_logger : logger
+val emacs_logger    : logger
+
+
+(** [set_feeder] A feeder processes the feedback, [ignore] by default *)
+val set_feeder : (feedback -> unit) -> unit
+
+(** [feedback ?id ?route fb] produces feedback fb, with [route] and
+    [id] set appropiatedly, if absent, it will use the defaults set by
+    [set_id_for_feedback] *)
+val feedback :
+  ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit
+
+(** [set_id_for_feedback route id] Set the defaults for feedback *)
+val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
+
+(** [with_output_to_file file f x] executes [f x] with logging
+    redirected to a file [file] *)
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+
+(** {6 output functions}
+
+[msg_notice] do not put any decoration on output by default. If
+possible don't mix it with goal output (prefer msg_info or
+msg_warning) so that interfaces can dispatch outputs easily. Once all
+interfaces use the xml-like protocol this constraint can be
+relaxed. *)
+(* Should we advertise these functions more? Should they be the ONLY
+   allowed way to output something? *)
+
+val msg_info : Pp.std_ppcmds -> unit
+(** Message that displays information, usually in verbose mode, such as [Foobar
+    is defined] *)
+
+val msg_notice : Pp.std_ppcmds -> unit
+(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
+
+val msg_warning : Pp.std_ppcmds -> unit
+(** Message indicating that something went wrong, but without serious
+    consequences. *)
+
+val msg_error : Pp.std_ppcmds -> unit
+(** Message indicating that something went really wrong, though still
+    recoverable; otherwise an exception would have been raised. *)
+
+val msg_debug : Pp.std_ppcmds -> unit
+(** For debugging purposes *)
+
+
+
+
diff --git a/lib/pp.ml b/lib/pp.ml
index e4c78ba73f..d07f01b906 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -64,13 +64,6 @@ end
 
 open Pp_control
 
-(* This should not be used outside of this file. Use
-   Flags.print_emacs instead. This one is updated when reading
-   command line options. This was the only way to make [Pp] depend on
-   an option without creating a circularity: [Flags] -> [Util] ->
-   [Pp] -> [Flags] *)
-let print_emacs = ref false
-
 (* The different kinds of blocks are:
    \begin{description}
    \item[hbox:] Horizontal block no line breaking;
@@ -339,175 +332,23 @@ let pp_dirs ?pp_tag ft =
       let () = Format.pp_print_flush ft () in
       Exninfo.iraise reraise
 
-
-
-(* pretty print on stdout and stderr *)
-
-(* Special chars for emacs, to detect warnings inside goal output *)
-let emacs_quote_start = String.make 1 (Char.chr 254)
-let emacs_quote_end = String.make 1 (Char.chr 255)
-
-let emacs_quote_info_start = "<infomsg>"
-let emacs_quote_info_end = "</infomsg>"
-
-let emacs_quote g =
-  if !print_emacs then hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
-  else hov 0 g
-
-let emacs_quote_info g =
-  if !print_emacs then hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
-  else hov 0 g
-
-
 (* pretty printing functions WITHOUT FLUSH *)
 let pp_with ?pp_tag ft strm =
   pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm))
 
-let ppnl_with ft strm =
-  pp_dirs ft (Glue.atom (Ppdir_ppcmds (strm ++ fnl ())))
-
 (* pretty printing functions WITH FLUSH *)
 let msg_with ft strm =
   pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush))
 
-let msgnl_with ft strm =
-  pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_newline))
-
-(* pretty printing functions WITHOUT FLUSH *)
-let pp        x = pp_with   !std_ft x
-let ppnl      x = ppnl_with !std_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 pp_flush  x = Format.pp_print_flush !std_ft x
-let pperr_flush x = Format.pp_print_flush !err_ft x
-let flush_all () =
-  flush stderr; flush stdout; pp_flush (); pperr_flush ()
-
-(* pretty printing functions WITH FLUSH *)
-let msg x = msg_with !std_ft x
-let msgnl x = msgnl_with !std_ft x
-let msgerr x = msg_with !err_ft x
-let msgerrnl x = msgnl_with !err_ft x
-
-(* Logging management *)
-
-type message_level =  Feedback.message_level =
-  | Debug of string
-  | Info
-  | Notice
-  | Warning
-  | Error
-
-type message = Feedback.message = {
-  message_level : message_level;
-  message_content : Xml_datatype.xml;
-}
-
-let of_message = Feedback.of_message
-let to_message = Feedback.to_message
-let is_message = Feedback.is_message
-
-type logger = message_level -> std_ppcmds -> unit
-
-let make_body info s =
-  emacs_quote (hov 0 (info ++ spc () ++ s))
-
-let debugbody strm = emacs_quote_info (hov 0 (str "Debug:" ++ spc () ++ strm))
-let warnbody strm = make_body (str "Warning:") strm
-let errorbody strm = make_body (str "Error:") strm
-let infobody strm = emacs_quote_info strm
-
-let std_logger ~id:_ level msg = match level with
-| Debug _ -> msgnl (debugbody msg)
-| Info -> msgnl (hov 0 msg)
-| Notice -> msgnl msg
-| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) ()
-| Error -> msgnl_with !err_ft (errorbody msg)
-
-let emacs_logger ~id:_ level mesg = match level with
-| Debug _ -> msgnl (debugbody mesg)
-| Info -> msgnl (infobody mesg)
-| Notice -> msgnl mesg
-| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody mesg)) ()
-| Error -> msgnl_with !err_ft (errorbody mesg)
-
-let logger = ref std_logger
-
-let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger
-let make_pp_nonemacs() = print_emacs:=false; logger := std_logger
-
-let ft_logger old_logger ft ~id level mesg = match level with
-  | Debug _ -> msgnl_with ft (debugbody mesg)
-  | Info -> msgnl_with ft (infobody mesg)
-  | Notice -> msgnl_with ft mesg
-  | Warning -> old_logger ~id:id level mesg
-  | Error -> old_logger ~id:id level mesg
-
-let with_output_to_file fname func input =
-  let old_logger = !logger in
-  let channel = open_out (String.concat "." [fname; "out"]) in
-  logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
-  try
-    let output = func input in
-    logger := old_logger;
-    close_out channel;
-    output
-  with reraise ->
-    let reraise = Backtrace.add_backtrace reraise in
-    logger := old_logger;
-    close_out channel;
-    Exninfo.iraise reraise
-
-let feedback_id = ref (Feedback.Edit 0)
-let feedback_route = ref Feedback.default_route
-
 (* If mixing some output and a goal display, please use msg_warning,
    so that interfaces (proofgeneral for example) can easily dispatch
    them to different windows. *)
 
-let msg_info x = !logger ~id:!feedback_id Info x
-let msg_notice x = !logger ~id:!feedback_id Notice x
-let msg_warning x = !logger ~id:!feedback_id Warning x
-let msg_error x = !logger ~id:!feedback_id Error x
-let msg_debug x = !logger ~id:!feedback_id (Debug "_") x
-
-let set_logger l = logger := (fun ~id:_ lvl msg -> l lvl msg)
-
-let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg
-
-(** Feedback *)
-
-let feeder = ref ignore
-let set_id_for_feedback ?(route=Feedback.default_route) i =
-  feedback_id := i; feedback_route := route
-let feedback ?state_id ?edit_id ?route what =
-  !feeder {
-     Feedback.contents = what;
-     Feedback.route = Option.default !feedback_route route;
-     Feedback.id =
-       match state_id, edit_id with
-       | Some id, _ -> Feedback.State id
-       | None, Some eid -> Feedback.Edit eid
-       | None, None -> !feedback_id;
-  }
-let set_feeder f = feeder := f
-let get_id_for_feedback () = !feedback_id, !feedback_route
-
-(** Utility *)
-
+(** Output to a string formatter *)
 let string_of_ppcmds c =
-  msg_with Format.str_formatter c;
+  Format.fprintf Format.str_formatter "@[%a@]" msg_with c;
   Format.flush_str_formatter ()
 
-let log_via_feedback printer = logger := (fun ~id lvl msg ->
-  !feeder {
-     Feedback.contents = Feedback.Message {
-       message_level = lvl;
-       message_content = printer msg };
-     Feedback.route = !feedback_route;
-     Feedback.id = id })
-
 (* Copy paste from Util *)
 
 let pr_comma () = str "," ++ spc ()
@@ -597,3 +438,4 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
 let prvect elem v = prvect_with_sep mt elem v
 
 let surround p = hov 1 (str"(" ++ p ++ str")")
+
diff --git a/lib/pp.mli b/lib/pp.mli
index 04a60a7c8d..ced4b66032 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,32 +6,24 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Modify pretty printing functions behavior for emacs ouput (special
-   chars inserted at some places). This function should called once in
-   module [Options], that's all. *)
-val make_pp_emacs:unit -> unit
-val make_pp_nonemacs:unit -> unit
-
-val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
-
 (** Pretty-printers. *)
 
 type std_ppcmds
 
 (** {6 Formatting commands} *)
 
-val str  : string -> std_ppcmds
+val str   : string -> std_ppcmds
 val stras : int * string -> std_ppcmds
-val brk : int * int -> std_ppcmds
-val tbrk : int * int -> std_ppcmds
-val tab : unit -> std_ppcmds
-val fnl : unit -> std_ppcmds
-val pifb : unit -> std_ppcmds
-val ws : int -> std_ppcmds
-val mt : unit -> std_ppcmds
-val ismt : std_ppcmds -> bool
-
-val comment : int -> std_ppcmds
+val brk   : int * int -> std_ppcmds
+val tbrk  : int * int -> std_ppcmds
+val tab   : unit -> std_ppcmds
+val fnl   : unit -> std_ppcmds
+val pifb  : unit -> std_ppcmds
+val ws    : int -> std_ppcmds
+val mt    : unit -> std_ppcmds
+val ismt  : std_ppcmds -> bool
+
+val comment  : int -> std_ppcmds
 val comments : ((int * int) * string) list ref
 
 (** {6 Manipulation commands} *)
@@ -100,87 +92,10 @@ sig
   (** Project an object from a tag. *)
 end
 
-type tag_handler = Tag.t -> Format.tag
-
 val tag : Tag.t -> std_ppcmds -> std_ppcmds
 val open_tag : Tag.t -> std_ppcmds
 val close_tag : unit -> std_ppcmds
 
-(** {6 Sending messages to the user} *)
-type message_level = Feedback.message_level =
-  | Debug of string
-  | Info
-  | Notice
-  | Warning
-  | Error
-
-type message = Feedback.message = {
-  message_level : message_level;
-  message_content : Xml_datatype.xml;
-}
-
-type logger = message_level -> std_ppcmds -> unit
-
-(** {6 output functions}
-
-[msg_notice] do not put any decoration on output by default. If
-possible don't mix it with goal output (prefer msg_info or
-msg_warning) so that interfaces can dispatch outputs easily. Once all
-interfaces use the xml-like protocol this constraint can be
-relaxed. *)
-(* Should we advertise these functions more? Should they be the ONLY
-   allowed way to output something? *)
-
-val msg_info : std_ppcmds -> unit
-(** Message that displays information, usually in verbose mode, such as [Foobar
-    is defined] *)
-
-val msg_notice : std_ppcmds -> unit
-(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
-
-val msg_warning : std_ppcmds -> unit
-(** Message indicating that something went wrong, but without serious
-    consequences. *)
-
-val msg_error : std_ppcmds -> unit
-(** Message indicating that something went really wrong, though still
-    recoverable; otherwise an exception would have been raised. *)
-
-val msg_debug : std_ppcmds -> unit
-(** For debugging purposes *)
-
-val std_logger : logger
-(** Standard logging function *)
-
-val set_logger : logger -> unit
-
-val log_via_feedback : (std_ppcmds -> Xml_datatype.xml) -> unit
-
-val of_message : message -> Xml_datatype.xml
-val to_message : Xml_datatype.xml -> message
-val is_message : Xml_datatype.xml -> bool
-
-
-(** {6 Feedback sent, even asynchronously, to the user interface} *)
-
-(* This stuff should be available to most of the system, line msg_* above.
- * But I'm unsure this is the right place, especially for the global edit_id.
- *
- * Morally the parser gets a string and an edit_id, and gives back an AST.
- * Feedbacks during the parsing phase are attached to this edit_id.
- * The interpreter assigns an exec_id to the ast, and feedbacks happening
- * during interpretation are attached to the exec_id.
- * Only one among state_id and edit_id can be provided. *)
-
-val feedback :
-  ?state_id:Feedback.state_id -> ?edit_id:Feedback.edit_id ->
-  ?route:Feedback.route_id -> Feedback.feedback_content -> unit
-
-val set_id_for_feedback :
-  ?route:Feedback.route_id -> Feedback.edit_or_state_id -> unit
-val set_feeder : (Feedback.feedback -> unit) -> unit
-val get_id_for_feedback : unit -> Feedback.edit_or_state_id * Feedback.route_id
-
 (** {6 Utilities} *)
 
 val string_of_ppcmds : std_ppcmds -> string
@@ -251,31 +166,9 @@ val surround : std_ppcmds -> std_ppcmds
 
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 
-(** {6 Low-level pretty-printing functions {% \emph{%}without flush{% }%}. } *)
-
-val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
+(** {6 Low-level pretty-printing functions with and without flush} *)
 
-(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
-
-(** These functions are low-level interface to printing and should not be used
-    in usual code. Consider using the [msg_*] function family instead. *)
-
-val pp : std_ppcmds -> unit
-val ppnl : std_ppcmds -> unit
-val pperr : std_ppcmds -> unit
-val pperrnl : std_ppcmds -> unit
-val pperr_flush : unit -> unit
-val pp_flush : unit -> unit
-val flush_all: unit -> unit
-
-(** {6 Deprecated functions} *)
-
-(** DEPRECATED. Do not use in newly written code. *)
-
-val msg_with : Format.formatter -> std_ppcmds -> unit
-
-val msg : std_ppcmds -> unit
-val msgnl : std_ppcmds -> unit
-val msgerr : std_ppcmds -> unit
-val msgerrnl : std_ppcmds -> unit
-val message : string -> unit       (** = pPNL *)
+(** FIXME: These ignore the logging settings and call [Format] directly *)
+type tag_handler = Tag.t -> Format.tag
+val msg_with :                        Format.formatter -> std_ppcmds -> unit
+val pp_with  : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
index 3ecaac0391..b068788c92 100644
--- a/lib/ppstyle.ml
+++ b/lib/ppstyle.ml
@@ -107,8 +107,11 @@ let pp_tag t = match Pp.Tag.prj t tag with
 | None -> ""
 | Some key -> key
 
+let clear_tag_fn = ref (fun () -> ())
+
 let init_color_output () =
   let push_tag, pop_tag, clear_tag = make_style_stack !tags in
+  clear_tag_fn := clear_tag;
   let tag_handler = {
     Format.mark_open_tag = push_tag;
     Format.mark_close_tag = pop_tag;
@@ -116,34 +119,23 @@ let init_color_output () =
     Format.print_close_tag = ignore;
   } in
   let open Pp_control in
-  let () = Format.pp_set_mark_tags !std_ft true in
-  let () = Format.pp_set_mark_tags !err_ft true in
-  let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in
-  let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in
+  Format.pp_set_mark_tags !std_ft true;
+  Format.pp_set_mark_tags !err_ft true;
+  Format.pp_set_formatter_tag_functions !std_ft tag_handler;
+  Format.pp_set_formatter_tag_functions !err_ft tag_handler
+
+let color_msg ?header ft strm =
   let pptag = tag in
   let open Pp in
-  let msg ?header ft strm =
-    let strm = match header with
+  let strm = match header with
     | None -> hov 0 strm
     | Some (h, t) ->
       let tag = Pp.Tag.inj t pptag in
       let h = Pp.tag tag (str h ++ str ":") in
       hov 0 (h ++ spc () ++ strm)
-    in
-    pp_with ~pp_tag ft strm;
-    Format.pp_print_newline ft ();
-    Format.pp_print_flush ft ();
-    (** In case something went wrong, we reset the stack *)
-    clear_tag ();
-  in
-  let logger level strm = match level with
-  | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm
-  | Info -> msg !std_ft strm
-  | Notice -> msg !std_ft strm
-  | Warning ->
-    let header = ("Warning", warning_tag) in
-    Flags.if_warn (fun () -> msg ~header !err_ft strm) ()
-  | Error -> msg ~header:("Error", error_tag) !err_ft strm
   in
-  let () = set_logger logger in
-  ()
+  pp_with ~pp_tag ft strm;
+  Format.pp_print_newline ft ();
+  Format.pp_print_flush ft ();
+  (** In case something went wrong, we reset the stack *)
+  !clear_tag_fn ()
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
index 97b5869f9b..1cd701ed4e 100644
--- a/lib/ppstyle.mli
+++ b/lib/ppstyle.mli
@@ -11,7 +11,8 @@
 
 (** {5 Style tags} *)
 
-type t
+type t = string
+
 (** Style tags *)
 
 val make : ?style:Terminal.style -> string list -> t
@@ -46,12 +47,11 @@ val dump : unit -> (t * Terminal.style option) list
 (** {5 Setting color output} *)
 
 val init_color_output : unit -> unit
-(** Once called, all tags defined here will use their current style when
-    printed. To this end, this function redefines the loggers used when sending
-    messages to the user. The program will in particular use the formatters
-    {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages,
-    with additional syle information provided by this module. Be careful this is
-    not compatible with the Emacs mode! *)
+
+val color_msg : ?header:string * Format.tag ->
+  Format.formatter -> Pp.std_ppcmds -> unit
+(** {!color_msg ?header fmt pp} will format according to the tags
+     defined in this file *)
 
 val pp_tag : Pp.tag_handler
 (** Returns the name of a style tag that is understandable by the formatters
diff --git a/lib/system.ml b/lib/system.ml
index e54109a2f3..8cdcaf5dcc 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -88,9 +88,9 @@ let all_subdirs ~unix_path:root =
       | _ -> ()
     in process_directory f path
   in
-  check_unix_dir (fun s -> msg_warning (str s)) root;
+  check_unix_dir (fun s -> Feedback.msg_warning (str s)) root;
   if exists_dir root then traverse root []
-  else msg_warning (str ("Cannot open " ^ root));
+  else Feedback.msg_warning (str ("Cannot open " ^ root));
   List.rev !l
 
 (* Caching directory contents for efficient syntactic equality of file
@@ -149,7 +149,7 @@ let where_in_path ?(warn=true) path filename =
   | (lpe, f) :: l' ->
     let () = match l' with
     | _ :: _ when warn ->
-      msg_warning
+      Feedback.msg_warning
         (str filename ++ str " has been found in" ++ spc () ++
           hov 0 (str "[ " ++
             hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
@@ -205,7 +205,7 @@ let is_in_system_path filename =
     let lpath = CUnix.path_to_list (Sys.getenv "PATH") in
     is_in_path lpath filename
   with Not_found ->
-    msg_warning (str "system variable PATH not found");
+    Feedback.msg_warning (str "system variable PATH not found");
     false
 
 let open_trapping_failure name =
@@ -216,7 +216,7 @@ let open_trapping_failure name =
 let try_remove filename =
   try Sys.remove filename
   with e when Errors.noncritical e ->
-    msg_warning
+    Feedback.msg_warning
       (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
 let error_corrupted file s =
@@ -345,13 +345,13 @@ let with_time time f x =
     let y = f x in
     let tend = get_time() in
     let msg2 = if time then "" else " (successful)" in
-    msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     y
   with e ->
     let tend = get_time() in
     let msg = if time then "" else "Finished failing transaction in " in
     let msg2 = if time then "" else " (failure)" in
-    msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
 
 let process_id () =