From c8852c570c980e35072ff40c84c375f84ec5f581 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 24 Nov 2014 14:33:57 +0100 Subject: Plugging console highlighting in for toplevel and compilation error messages. --- printing/ppstyle.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'printing/ppstyle.ml') diff --git a/printing/ppstyle.ml b/printing/ppstyle.ml index 9839b627b..5585d4b7f 100644 --- a/printing/ppstyle.ml +++ b/printing/ppstyle.ml @@ -103,6 +103,10 @@ let debug_tag = let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA () in make ~style ["message"; "debug"] +let pp_tag t = match Pp.Tag.prj t tag with +| None -> "" +| Some key -> key + let init_color_output () = let push_tag, pop_tag, clear_tag = make_style_stack !tags in let tag_handler = { @@ -111,10 +115,6 @@ let init_color_output () = Format.print_open_tag = ignore; Format.print_close_tag = ignore; } in - let pp_tag t = match Pp.Tag.prj t tag with - | None -> "" - | Some key -> key - in let open Pp_control in let () = Format.pp_set_mark_tags !std_ft true in let () = Format.pp_set_mark_tags !err_ft true in -- cgit v1.2.3