diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-22 18:23:41 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-22 19:50:18 +0100 |
| commit | bd458575ba7f767e3b939fad5d628a9cb24e6bb2 (patch) | |
| tree | a547c45b8a886c94e3c7f461634039f75a8c8d30 /vernac | |
| parent | 8b73fd7c6ce423f8c8a2594e90200f2407795d52 (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.ml | 1 | ||||
| -rw-r--r-- | vernac/topfmt.mli | 1 |
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 |