diff options
| author | Maxime Dénès | 2017-04-04 17:22:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-04 17:22:33 +0200 |
| commit | f22c72ff594408c3a3cac04cfee2234a59f2655b (patch) | |
| tree | ef1b5370fbcd448d063ca92564fba311e424fdf5 /vernac | |
| parent | ea10a2da9ac11ea57e9eb80d0d6baf9321886da4 (diff) | |
| parent | bd458575ba7f767e3b939fad5d628a9cb24e6bb2 (diff) | |
Merge PR#502: [pp] Add anomaly header to error messages.
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 f843484f7e..e3c0a1709a 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 1555f80a9f..0e122f46e3 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 |