From e1f25889f88e078dac0f3b454eb16a470dd5f9ae Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 25 Jun 2016 18:59:39 +0200
Subject: [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.
---
 lib/feedback.mli | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'lib/feedback.mli')

diff --git a/lib/feedback.mli b/lib/feedback.mli
index 48b1c19a67..5160bd5bc1 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
-- 
cgit v1.2.3