[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.

1 files changed, 1 insertions, 0 deletions

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