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 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 47d433d79..65ffa6f84 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -61,8 +61,7 @@ let init_color () = match colors with | None -> (** Default colors *) - Ppstyle.init_color_output (); - Feedback.set_logger Feedback.color_terminal_logger + Feedback.init_color_output () | Some "" -> (** No color output *) () @@ -70,8 +69,7 @@ let init_color () = (** Overwrite all colors *) Ppstyle.clear_styles (); Ppstyle.parse_config s; - Ppstyle.init_color_output (); - Feedback.set_logger Feedback.color_terminal_logger + Feedback.init_color_output () end let toploop_init = ref begin fun x -> |