diff options
| -rw-r--r-- | lib/cErrors.ml | 5 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 4 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 1 | ||||
| -rw-r--r-- | vernac/topfmt.mli | 1 |
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 |