diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-24 14:33:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-24 14:33:57 +0100 |
| commit | c8852c570c980e35072ff40c84c375f84ec5f581 (patch) | |
| tree | 15bc4e2fddd85279045705ba8fb4960cbd84e6b7 /printing/ppstyle.ml | |
| parent | c96bde02138e00ba8800733e4ca2f1915b4c0c6f (diff) | |
Plugging console highlighting in for toplevel and compilation error messages.
Diffstat (limited to 'printing/ppstyle.ml')
| -rw-r--r-- | printing/ppstyle.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |