From 07432c05d3c814ae694f4b817be5e1589b8202ff Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 5 Apr 2018 18:41:30 +0200 Subject: Making explicit that errors happen in one of five executation phases. The five phases are command line interpretation, initialization, prelude loading, rcfile loading, and sentence interpretation (only the two latters are located). We then parameterize the feedback handler with the given execution phase, so as to possibly annotate the message with information pertaining to the phase. --- vernac/topfmt.mli | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'vernac/topfmt.mli') diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 579b456a2..73dcb0064 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -53,8 +53,17 @@ val init_terminal_output : color:bool -> unit (** Error printing *) (* To be deprecated when we can fully move to feedback-based error printing. *) + +type execution_phase = + | ParsingCommandLine + | Initialization + | LoadingPrelude + | LoadingRcFile + | InteractiveLoop + val pr_loc : Loc.t -> Pp.t -val print_err_exn : ?extra:Pp.t -> exn -> unit +val pr_phase : ?loc:Loc.t -> execution_phase -> Pp.t option +val print_err_exn : execution_phase -> exn -> unit (** [with_output_to_file file f x] executes [f x] with logging redirected to a file [file] *) -- cgit v1.2.3