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/pp.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/pp.mli') 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 -- cgit v1.2.3