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/pp.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/pp.mli')
| -rw-r--r-- | lib/pp.mli | 6 |
1 files changed, 3 insertions, 3 deletions
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 |