From 4abb41d008fc754f21916dcac9cce49f2d04dd6d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 24 Apr 2017 19:25:48 +0200 Subject: [toplevel] Use exception information for error printing. This is a partial backtrack on 63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we disregarded exception and tried to print error messages just by listening to feedback. However, feedback error messages are not always emitted due to https://coq.inria.fr/bugs/show_bug.cgi?id=5479 Thus meanwhile it is safer to go back to printing the information present in exceptions until we tweak the STM. This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many other glitches not reported, such errors in nested proofs. --- vernac/topfmt.mli | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'vernac/topfmt.mli') diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 909dd7077..6c8e0ae2f 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -36,19 +36,22 @@ val get_depth_boxes : unit -> int option val set_margin : int option -> unit 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, 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 +(** Color output *) val init_color_output : unit -> unit val clear_styles : unit -> unit val parse_color_config : string -> unit val dump_tags : unit -> (string * Terminal.style) list +(** Error printing *) +(* To be deprecated when we can fully move to feedback-based error + printing. *) +val pr_loc : Loc.t -> Pp.std_ppcmds +val print_err_exn : ?extra:Pp.std_ppcmds -> exn -> unit + (** [with_output_to_file file f x] executes [f x] with logging redirected to a file [file] *) val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b -- cgit v1.2.3