diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-05 18:41:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-02 22:25:44 +0200 |
| commit | 07432c05d3c814ae694f4b817be5e1589b8202ff (patch) | |
| tree | e08529d454a12b8abc15c040abdfc9cc610b8660 /vernac/topfmt.mli | |
| parent | aae89bce1ca7c1a21b7eef345050dff5a9e88748 (diff) | |
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.
Diffstat (limited to 'vernac/topfmt.mli')
| -rw-r--r-- | vernac/topfmt.mli | 11 |
1 files changed, 10 insertions, 1 deletions
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] *) |