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