[pp] Add anomaly header to anomaly error messages.

This patch restores the proper printing of anomalies in coqtop / coqc
/ coqide. Currently, they are printed with an `Error` header, whereas
they should be printed with an `Anomaly" header.

This reopens an unfinished debate started in #390 , about how to
properly do "message" headers. Prior to #390, headers were handled
inconsistently, sometimes, `Error` or `Anomaly` were added in
`CErrors`, which lives below of the tagging system, thus some times we
got no coloring (c.f. https://coq.inria.fr/bugs/show_bug.cgi?id=4789),
but some other times the headers were added by the message handlers in
Feedback.

PR #390 takes the position of identifying the messages with the
`Feedback.level` tag, and letting the backends to the tagging. This
makes sense as the backends may want to interpret the "headers" in any
way they'd like. For instance, instead of printing: `Error: foo` they
may want to insert an image.

Note that this implies that CoqIDE doesn't currently insert an error
header on the first error case. This could be easily solved, but for
anomalies we could do in any of the ways explained below.

There are thus two natural ways to handle anomalies here: One is to
tag them as errors, but add a text header, this is done now, with the
small optimization in the case the handled has access to the exception
itself. The second way is to add a new `Feedback.level` category and
tag the anomalies appropriately. We would need also to modify Fail in
this case, or to completely remove it from the protocol.

I guess feedback from the rest of developers is needed before
committing to a strategy, for now this patch should be good.

4 files changed, 7 insertions, 4 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 99b763602..1c1ff7e2f 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -92,9 +92,8 @@ let print_backtrace e = match Backtrace.get_backtrace e with
 
 let print_anomaly askreport e =
   if askreport then
-    hov 0 (raw_anomaly e ++ spc () ++
-           strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
-           str ".")
+    hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e) ++ spc ()) ++
+    hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")
   else
     hov 0 (raw_anomaly e)
 
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 0cc6ca317..bbe4fb84c 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -252,7 +252,9 @@ let print_toplevel_error (e, info) =
       else mt ()
     else print_location_in_file loc
   in
-  let hdr msg = hov 0 (Topfmt.err_hdr ++ msg) in
+  let hdr_text =
+    if CErrors.is_anomaly e then Topfmt.ann_hdr else Topfmt.err_hdr in
+  let hdr msg = hov 0 (hdr_text ++ msg) in
   locmsg ++ hdr (CErrors.iprint (e, info))
 
 (* Read the input stream until a dot is encountered *)
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index f843484f7..e3c0a1709 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -136,6 +136,7 @@ let  dbg_hdr = tag Tag.debug   (str "Debug:")   ++ spc ()
 let info_hdr = mt ()
 let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
 let  err_hdr = tag Tag.error   (str "Error:")   ++ spc ()
+let  ann_hdr = tag Tag.error   (str "Anomaly:") ++ spc ()
 
 let make_body quoter info ?loc s =
   let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 1555f80a9..0e122f46e 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -38,6 +38,7 @@ val get_margin : unit -> int option
 
 (** Headers for tagging *)
 val err_hdr : Pp.std_ppcmds
+val ann_hdr : Pp.std_ppcmds
 
 (** Console display of feedback *)
 val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit