diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-25 18:59:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-09-30 09:44:00 +0200 |
| commit | e1f25889f88e078dac0f3b454eb16a470dd5f9ae (patch) | |
| tree | 435ddbc8b2fa093508548e0d40a391ccf6b144d0 /lib/feedback.mli | |
| parent | 6d20e4c136fb2726ec8577bdfee051ecacdf8261 (diff) | |
[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.
Diffstat (limited to 'lib/feedback.mli')
| -rw-r--r-- | lib/feedback.mli | 7 |
1 files changed, 2 insertions, 5 deletions
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 |