From 63cfc77ddf3586262d905dc351b58669d185a55e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 31 Mar 2017 20:38:52 +0200 Subject: [toplevel] Remove exception error printer in favor of feedback printer. We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429 --- vernac/topfmt.mli | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'vernac/topfmt.mli') diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 0e122f46e..909dd7077 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -40,10 +40,9 @@ val get_margin : unit -> int option 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 - -val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit +(** Console display of feedback, we may add some location information *) +val std_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit +val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit val init_color_output : unit -> unit val clear_styles : unit -> unit -- cgit v1.2.3