[pp] Remove duplicate color logger.

We use the same printing path for color and mono terminal output, thus
removing the duplicate printers which avoids problems as they don't have
to be kept in sync anymore.

We tag unconditionally but set the `pp_tag` tagger properly. This
removes IO from `Ppstyle` with IMO is the right thing to do.

Test suite passes.

7 files changed, 90 insertions, 117 deletions

diff --git a/lib/feedback.ml b/lib/feedback.ml
index dd1ca2af3..44b3ee35d 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -52,8 +52,7 @@ open Pp_control
 
 type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
 
-let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ())
-let msgnl          strm = msgnl_with !std_ft strm
+let msgnl_with ?pp_tag fmt strm = msg_with ?pp_tag fmt (strm ++ fnl ())
 
 (* XXX: This is really painful! *)
 module Emacs = struct
@@ -75,45 +74,100 @@ end
 
 open Emacs
 
-let  dbg_str = str "Debug:"   ++ spc ()
+let  dbg_str = tag Ppstyle.(Tag.inj debug_tag   tag) (str "Debug:")   ++ spc ()
 let info_str = mt ()
-let warn_str = str "Warning:" ++ spc ()
-let  err_str = str "Error:"   ++ spc ()
+let warn_str = tag Ppstyle.(Tag.inj warning_tag tag) (str "Warning:") ++ spc ()
+let  err_str = tag Ppstyle.(Tag.inj error_tag   tag) (str "Error:"  ) ++ spc ()
 
 let make_body quoter info ?loc s =
   let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
   quoter (hov 0 (loc ++ info ++ s))
 
 (* Generic logger *)
-let gen_logger dbg err ?loc level msg = match level with
-  | Debug   -> msgnl (make_body dbg  dbg_str ?loc msg)
-  | Info    -> msgnl (make_body dbg info_str ?loc msg)
-  (* XXX: What to do with loc here? *)
-  | Notice  -> msgnl msg
+let gen_logger dbg err ?pp_tag ?loc level msg = match level with
+  | Debug   -> msgnl_with ?pp_tag !std_ft (make_body dbg  dbg_str ?loc msg)
+  | Info    -> msgnl_with ?pp_tag !std_ft (make_body dbg info_str ?loc msg)
+  | Notice  -> msgnl_with ?pp_tag !std_ft msg
   | Warning -> Flags.if_warn (fun () ->
-               msgnl_with !err_ft (make_body err warn_str ?loc msg)) ()
-  | Error   -> msgnl_with !err_ft (make_body err  err_str ?loc msg)
+               msgnl_with ?pp_tag !err_ft (make_body err warn_str ?loc msg)) ()
+  | Error   -> msgnl_with ?pp_tag !err_ft (make_body err  err_str ?loc msg)
 
-(** Standard loggers *)
-let std_logger  = gen_logger (fun x -> x) (fun x -> x)
+(* We provide a generic clear_log_backend callback for backends
+   wanting to do clenaup after the print.
+*)
+let std_logger_tag     = ref None
+let std_logger_cleanup = ref (fun () -> ())
 
-(* Color logger *)
-let color_terminal_logger ?loc level strm =
-  let msg  = Ppstyle.color_msg in
-  match level with
-  | Debug   -> msg ?loc ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
-  | Info    -> msg ?loc !std_ft strm
-  | Notice  -> msg ?loc !std_ft strm
-  | Warning -> Flags.if_warn (fun () ->
-               msg ?loc ~header:("Warning", Ppstyle.warning_tag) !err_ft strm) ()
-  | Error   -> msg ?loc ~header:("Error",   Ppstyle.error_tag)   !err_ft strm
+let std_logger ?loc level msg =
+  gen_logger (fun x -> x) (fun x -> x) ?pp_tag:!std_logger_tag ?loc level msg;
+  !std_logger_cleanup ()
 
 (* Rules for emacs:
    - Debug/info: emacs_quote_info
    - Warning/Error: emacs_quote_err
    - Notice: unquoted
+
+  Note the inconsistency.
  *)
-let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
+let emacs_logger = gen_logger emacs_quote_info emacs_quote_err ?pp_tag:None
+
+(** Color logging. Moved from pp_style, it may need some more refactoring  *)
+
+(** Not thread-safe. We should put a lock somewhere if we print from
+    different threads. Do we? *)
+let make_style_stack () =
+  (** Default tag is to reset everything *)
+  let empty = Terminal.make () in
+  let default_tag = Terminal.({
+      fg_color = Some `DEFAULT;
+      bg_color = Some `DEFAULT;
+      bold = Some false;
+      italic = Some false;
+      underline = Some false;
+      negative = Some false;
+    })
+  in
+  let style_stack = ref [] in
+  let peek () = match !style_stack with
+  | []      -> default_tag  (** Anomalous case, but for robustness *)
+  | st :: _ -> st
+  in
+  let push tag =
+    let style = match Ppstyle.get_style tag with
+      | None    -> empty
+      | Some st -> st
+    in
+    (** Use the merging of the latest tag and the one being currently pushed.
+    This may be useful if for instance the latest tag changes the background and
+    the current one the foreground, so that the two effects are additioned. *)
+    let style = Terminal.merge (peek ()) style in
+    style_stack := style :: !style_stack;
+    Terminal.eval style
+  in
+  let pop _ = match !style_stack with
+  | []       -> (** Something went wrong, we fallback *)
+                Terminal.eval default_tag
+  | _ :: rem -> style_stack := rem;
+                Terminal.eval (peek ())
+  in
+  let clear () = style_stack := [] in
+  push, pop, clear
+
+let init_color_output () =
+  let open Pp_control in
+  let push_tag, pop_tag, clear_tag = make_style_stack () in
+  std_logger_cleanup := clear_tag;
+  std_logger_tag     := Some Ppstyle.pp_tag;
+  let tag_handler = {
+    Format.mark_open_tag   = push_tag;
+    Format.mark_close_tag  = pop_tag;
+    Format.print_open_tag  = ignore;
+    Format.print_close_tag = ignore;
+  } 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 logger       = ref std_logger
 let set_logger l = logger := l
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 48b1c19a6..5160bd5bc 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -72,11 +72,8 @@ 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!  *)
+(** [init_color_output ()] Enable color in the std_logger *)
+val init_color_output : unit -> unit
 
 (** [feedback_logger] will produce feedback messages instead IO events *)
 val feedback_logger : logger
diff --git a/lib/pp.ml b/lib/pp.ml
index 7f4bc149d..6eaad6fa6 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -356,8 +356,8 @@ let pp_with ?pp_tag ft strm =
   pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm))
 
 (* pretty printing functions WITH FLUSH *)
-let msg_with ft strm =
-  pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush))
+let msg_with ?pp_tag ft strm =
+  pp_dirs ?pp_tag ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush))
 
 (* If mixing some output and a goal display, please use msg_warning,
    so that interfaces (proofgeneral for example) can easily dispatch
@@ -365,7 +365,7 @@ let msg_with ft strm =
 
 (** Output to a string formatter *)
 let string_of_ppcmds c =
-  Format.fprintf Format.str_formatter "@[%a@]" msg_with c;
+  Format.fprintf Format.str_formatter "@[%a@]" (msg_with ?pp_tag:None) c;
   Format.flush_str_formatter ()
 
 (* Copy paste from Util *)
diff --git a/lib/pp.mli b/lib/pp.mli
index 3bd560812..e6542bae5 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -173,8 +173,8 @@ val pr_loc : Loc.t -> std_ppcmds
 (** FIXME: These ignore the logging settings and call [Format] directly *)
 type tag_handler = Tag.t -> Format.tag
 
-(** [msg_with fmt pp] Print [pp] to [fmt] and flush [fmt]  *)
-val msg_with :                        Format.formatter -> std_ppcmds -> unit
+(** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and flush [fmt]  *)
+val msg_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
 
-(** [msg_with fmt pp] Print [pp] to [fmt] and don't flush [fmt]  *)
+(** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and don't flush [fmt]  *)
 val pp_with  : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
index ecfaa822c..aa47c5167 100644
--- a/lib/ppstyle.ml
+++ b/lib/ppstyle.ml
@@ -56,41 +56,6 @@ let default = Terminal.({
 
 let empty = Terminal.make ()
 
-let make_style_stack style_tags =
-  (** Not thread-safe. We should put a lock somewhere if we print from
-      different threads. Do we? *)
-  let style_stack = ref [] in
-  let peek () = match !style_stack with
-  | [] -> default (** Anomalous case, but for robustness *)
-  | st :: _ -> st
-  in
-  let push tag =
-    let style =
-      try
-        begin match String.Map.find tag style_tags with
-        | None -> empty
-        | Some st -> st
-        end
-      with Not_found -> empty
-    in
-    (** Use the merging of the latest tag and the one being currently pushed.
-    This may be useful if for instance the latest tag changes the background and
-    the current one the foreground, so that the two effects are additioned. *)
-    let style = Terminal.merge (peek ()) style in
-    let () = style_stack := style :: !style_stack in
-    Terminal.eval style
-  in
-  let pop _ = match !style_stack with
-  | [] ->
-    (** Something went wrong, we fallback *)
-    Terminal.eval default
-  | _ :: rem ->
-    let () = style_stack := rem in
-    Terminal.eval (peek ())
-  in
-  let clear () = style_stack := [] in
-  push, pop, clear
-
 let error_tag =
   let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in
   make ~style ["message"; "error"]
@@ -106,37 +71,3 @@ let debug_tag =
 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;
-    Format.print_open_tag = ignore;
-    Format.print_close_tag = ignore;
-  } in
-  let open Pp_control 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 ?loc ?header ft strm =
-  let pptag = tag in
-  let open Pp in
-  let ploc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
-  let strm = match header with
-    | None -> hov 0 (ploc ++ strm)
-    | Some (h, t) ->
-      let tag = Pp.Tag.inj t pptag in
-      let h = Pp.tag tag (str h ++ str ":") in
-      hov 0 (ploc ++ 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_fn ()
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
index b07fcd5d4..d9fd75765 100644
--- a/lib/ppstyle.mli
+++ b/lib/ppstyle.mli
@@ -44,14 +44,7 @@ val parse_config : string -> unit
 val dump : unit -> (t * Terminal.style option) list
 (** Recover the list of known tags together with their current style. *)
 
-(** {5 Setting color output} *)
-
-val init_color_output : unit -> unit
-
-val color_msg : ?loc:Loc.t -> ?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 *)
+(** {5 Color output} *)
 
 val pp_tag : Pp.tag_handler
 (** Returns the name of a style tag that is understandable by the formatters
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 47d433d79..65ffa6f84 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -61,8 +61,7 @@ let init_color () =
     match colors with
     | None ->
       (** Default colors *)
-      Ppstyle.init_color_output ();
-      Feedback.set_logger Feedback.color_terminal_logger
+      Feedback.init_color_output ()
     | Some "" ->
       (** No color output *)
       ()
@@ -70,8 +69,7 @@ let init_color () =
       (** Overwrite all colors *)
       Ppstyle.clear_styles ();
       Ppstyle.parse_config s;
-      Ppstyle.init_color_output ();
-      Feedback.set_logger Feedback.color_terminal_logger
+      Feedback.init_color_output ()
   end
 
 let toploop_init = ref begin fun x ->