diff options
Diffstat (limited to 'vernac/topfmt.ml')
| -rw-r--r-- | vernac/topfmt.ml | 30 |
1 files changed, 18 insertions, 12 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 6a10eb43a..4e4077f42 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -1,12 +1,13 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Feedback open Pp (** Pp control also belongs here as the terminal is private to the toplevel *) @@ -138,7 +139,7 @@ let make_body quoter info ?pre_hdr s = (* The empty quoter *) let noq x = x (* Generic logger *) -let gen_logger dbg warn ?pre_hdr level msg = match level with +let gen_logger dbg warn ?pre_hdr level msg = let open Feedback in match level with | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?pre_hdr msg) | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg) | Notice -> msgnl_with !std_ft (make_body noq info_hdr ?pre_hdr msg) @@ -288,7 +289,6 @@ let init_terminal_output ~color = *) let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning - (* This is specific to the toplevel *) let pr_loc loc = let fname = loc.Loc.fname in @@ -311,17 +311,23 @@ let print_err_exn ?extra any = std_logger ~pre_hdr Feedback.Error msg let with_output_to_file fname func input = - (* XXX FIXME: redirect std_ft *) - (* let old_logger = !logger in *) let channel = open_out (String.concat "." [fname; "out"]) in - (* logger := ft_logger old_logger (Format.formatter_of_out_channel channel); *) + let old_fmt = !std_ft, !err_ft, !deep_ft in + let new_ft = Format.formatter_of_out_channel channel in + std_ft := new_ft; + err_ft := new_ft; + deep_ft := new_ft; try let output = func input in - (* logger := old_logger; *) + std_ft := Util.pi1 old_fmt; + err_ft := Util.pi2 old_fmt; + deep_ft := Util.pi3 old_fmt; close_out channel; output with reraise -> let reraise = Backtrace.add_backtrace reraise in - (* logger := old_logger; *) + std_ft := Util.pi1 old_fmt; + err_ft := Util.pi2 old_fmt; + deep_ft := Util.pi3 old_fmt; close_out channel; Exninfo.iraise reraise |