[pp] Try to properly tag error messages in cError.

In order to get proper coloring, we must tag the headers of error
messages in `CError`.

This should fix bug
https://coq.inria.fr/bugs/show_bug.cgi?id=5135

However, note that this could interact badly with the richpp printing
used by the IDE. At this level, we have no clue which tag we'd like to
apply, as we know (and shouldn't) nothing about the top level backend.

Thus, for now I've selected the console printer, hoping that the
`Richpp` won't crash the IDE.

3 files changed, 18 insertions, 5 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index c69c7e400..5c56192fc 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -16,6 +16,16 @@ let push = Backtrace.add_backtrace
 
 exception Anomaly of string option * std_ppcmds (* System errors *)
 
+(* XXX: To move to common tagging functions in Pp, blocked on tag
+ * system cleanup as we cannot define generic error tags now.
+ *
+ * Anyways, tagging should not happen here, but in the specific
+ * listener to the msg_* stuff.
+ *)
+let tag_err_str s = tag Ppstyle.(Tag.inj error_tag tag) (str s) ++ spc ()
+let err_str       = tag_err_str "Error:"
+let ann_str       = tag_err_str "Anomaly:"
+
 let _ =
   let pr = function
   | Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"")
@@ -93,7 +103,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with
 
 let print_anomaly askreport e =
   if askreport then
-    hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++
+    hov 0 (ann_str ++ raw_anomaly e ++ spc () ++
            strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
            str ".")
   else
@@ -115,7 +125,7 @@ let iprint_no_report (e, info) =
 
 let _ = register_handler begin function
   | UserError(s, pps) ->
-    hov 0 (str "Error: " ++ where (Some s) ++ pps)
+    hov 0 (err_str ++ where (Some s) ++ pps)
   | _ -> raise Unhandled
 end
 
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 1633ad976..e665db47d 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -2,7 +2,8 @@ File "stdin", line 1, characters 0-36:
 Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
 [arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+Error:
+To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
 File "stdin", line 2, characters 0-25:
 Warning: Ignoring rename of A into T. Only implicit arguments can be renamed.
@@ -125,5 +126,6 @@ File "stdin", line 53, characters 0-26:
 Warning: Ignoring rename of x into s. Only implicit arguments can be renamed.
 [arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+Error:
+To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index f4254e4e2..a2d545202 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,5 +1,6 @@
 The command has indeed failed with message:
-Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
+Error:
+Ltac variable y depends on pattern variable name z which is not bound in current context.
 Ltac f x y z :=
   symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
    dependent z