diff options
| author | Emilio Jesus Gallego Arias | 2018-11-08 20:52:06 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-09 00:33:31 +0100 |
| commit | d5aaa0ff95ce811dbca6644dad8bde70f7739514 (patch) | |
| tree | ca1e7306263ff242832f97a4df929ba15ceab2aa /vernac | |
| parent | 31825dc11a8e7fea42702182a3015067b0ed1140 (diff) | |
[topfmt] Add phase attribute for toplevel printing.
This is localized version of #8833, but instead of adding a phase
attribute which, as pointed by @gares has some problematic semantics,
we add a local one to the toplevel functions.
This moves the imperative part of the API to a better-delimited scope
and allows to progress with the separation of the interactive and
compilation API.
Note that still quite a few issues do remain in the "Feedback" path,
for example, idetop and other feedback clients cannot get a hold of
the feedback early enough as to direct init messages to the IDE part.
This is for example a serious issue of the API that shall be treated
separately.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/topfmt.ml | 22 | ||||
| -rw-r--r-- | vernac/topfmt.mli | 6 |
2 files changed, 22 insertions, 6 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index f842ca5ead..4bf76dae51 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -335,6 +335,20 @@ type execution_phase = | LoadingRcFile | InteractiveLoop +let default_phase = ref InteractiveLoop + +let in_phase ~phase f x = + let op = !default_phase in + default_phase := phase; + try + let res = f x in + default_phase := op; + res + with exn -> + let iexn = Backtrace.add_backtrace exn in + default_phase := op; + Util.iraise iexn + let pr_loc loc = let fname = loc.Loc.fname in match fname with @@ -347,8 +361,8 @@ let pr_loc loc = int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ str":") -let pr_phase ?loc phase = - match phase, loc with +let pr_phase ?loc () = + match !default_phase, loc with | LoadingRcFile, loc -> (* For when all errors go through feedback: str "While loading rcfile:" ++ @@ -363,10 +377,10 @@ let pr_phase ?loc phase = (* Note: interactive messages such as "foo is defined" are not located *) None -let print_err_exn phase any = +let print_err_exn any = let (e, info) = CErrors.push any in let loc = Loc.get_loc info in - let pre_hdr = pr_phase ?loc phase in + let pre_hdr = pr_phase ?loc () in let msg = CErrors.iprint (e, info) ++ fnl () in std_logger ?pre_hdr Feedback.Error msg diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 73dcb0064b..0ddf474970 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -61,9 +61,11 @@ type execution_phase = | LoadingRcFile | InteractiveLoop +val in_phase : phase:execution_phase -> ('a -> 'b) -> 'a -> 'b + val pr_loc : Loc.t -> Pp.t -val pr_phase : ?loc:Loc.t -> execution_phase -> Pp.t option -val print_err_exn : execution_phase -> exn -> unit +val pr_phase : ?loc:Loc.t -> unit -> Pp.t option +val print_err_exn : exn -> unit (** [with_output_to_file file f x] executes [f x] with logging redirected to a file [file] *) |