diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 19:25:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 18:43:03 +0200 |
| commit | 4abb41d008fc754f21916dcac9cce49f2d04dd6d (patch) | |
| tree | 3823e5c3706386d8bf997b5d8d25b42b81f2347d /vernac/topfmt.mli | |
| parent | 0fd7d060e0872a6ae3662dfb7a1fb940b80ef9df (diff) | |
[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.
Diffstat (limited to 'vernac/topfmt.mli')
| -rw-r--r-- | vernac/topfmt.mli | 11 |
1 files changed, 7 insertions, 4 deletions
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 |