Plugging console highlighting in for toplevel and compilation error messages.

4 files changed, 14 insertions, 6 deletions

diff --git a/printing/ppstyle.ml b/printing/ppstyle.ml
index 9839b627b1..5585d4b7ff 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
diff --git a/printing/ppstyle.mli b/printing/ppstyle.mli
index e6e664f79b..b6aa0e694c 100644
--- a/printing/ppstyle.mli
+++ b/printing/ppstyle.mli
@@ -53,6 +53,11 @@ val init_color_output : unit -> unit
     with additional syle information provided by this module. Be careful this is
     not compatible with the Emacs mode! *)
 
+val pp_tag : Pp.tag_handler
+(** Returns the name of a style tag that is understandable by the formatters
+    that have been inititialized through {!init_color_output}. To be used with
+    {!Pp.pp_with}. *)
+
 (** {5 Tags} *)
 
 val error_tag : t
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 3f93588904..c29b52cec0 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -323,7 +323,8 @@ let do_vernac () =
         else ppnl (str"Error: There is no ML toplevel." ++ fnl ())
     | any ->
         Format.set_formatter_out_channel stdout;
-        ppnl (print_toplevel_error any);
+        let msg = print_toplevel_error any ++ fnl () in
+        pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
         pp_flush ()
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 4580e49b1c..913dcded42 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -21,7 +21,9 @@ let () = at_exit flush_all
 let ( / ) = Filename.concat
 
 let fatal_error info anomaly =
-  pperrnl info; flush_all ();
+  let msg = info ++ fnl () in
+  pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg;
+  flush_all ();
   exit (if anomaly then 129 else 1)
 
 let get_version_date () =