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.ml | |
| 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.ml')
| -rw-r--r-- | vernac/topfmt.ml | 31 |
1 files changed, 27 insertions, 4 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 055f6676e..dbfad51a6 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -289,6 +289,14 @@ let init_terminal_output ~color = let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning (* This is specific to the toplevel *) + +type execution_phase = + | ParsingCommandLine + | Initialization + | LoadingPrelude + | LoadingRcFile + | InteractiveLoop + let pr_loc loc = let fname = loc.Loc.fname in match fname with @@ -301,13 +309,28 @@ let pr_loc loc = int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ str":") -let print_err_exn ?extra any = +let pr_phase ?loc phase = + match phase, loc with + | LoadingRcFile, loc -> + (* For when all errors go through feedback: + str "While loading rcfile:" ++ + Option.cata (fun loc -> fnl () ++ pr_loc loc) (mt ()) loc *) + Option.map pr_loc loc + | LoadingPrelude, loc -> + Some (str "While loading initial state:" ++ Option.cata (fun loc -> fnl () ++ pr_loc loc) (mt ()) loc) + | _, Some loc -> Some (pr_loc loc) + | ParsingCommandLine, _ + | Initialization, _ -> None + | InteractiveLoop, _ -> + (* Note: interactive messages such as "foo is defined" are not located *) + None + +let print_err_exn phase any = let (e, info) = CErrors.push any in let loc = Loc.get_loc info in - let msg_loc = Option.cata pr_loc (mt ()) loc in - let pre_hdr = pr_opt_no_spc (fun x -> x) extra ++ msg_loc in + let pre_hdr = pr_phase ?loc phase in let msg = CErrors.iprint (e, info) ++ fnl () in - std_logger ~pre_hdr Feedback.Error msg + std_logger ?pre_hdr Feedback.Error msg let with_output_to_file fname func input = let channel = open_out (String.concat "." [fname; "out"]) in |