aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-22 18:23:41 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-22 19:50:18 +0100
commitbd458575ba7f767e3b939fad5d628a9cb24e6bb2 (patch)
treea547c45b8a886c94e3c7f461634039f75a8c8d30 /vernac
parent8b73fd7c6ce423f8c8a2594e90200f2407795d52 (diff)
[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.
Diffstat (limited to 'vernac')
-rw-r--r--vernac/topfmt.ml1
-rw-r--r--vernac/topfmt.mli1
2 files changed, 2 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
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