diff options
Diffstat (limited to 'vernac/topfmt.ml')
| -rw-r--r-- | vernac/topfmt.ml | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index a1835959c..e44b585d7 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -106,8 +106,6 @@ module Tag = struct end -type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit - let msgnl_with ?pre_hdr fmt strm = pp_with fmt (strm ++ fnl ()); Format.pp_print_flush fmt () @@ -283,16 +281,6 @@ let print_err_exn ?extra any = let msg = CErrors.iprint (e, info) ++ fnl () in std_logger ~pre_hdr Feedback.Error msg -(* Output to file, used only in extraction so a candidate for removal *) -let ft_logger old_logger ft ?loc level mesg = - let id x = x in - match level with - | Debug -> msgnl_with ft (make_body id dbg_hdr mesg) - | Info -> msgnl_with ft (make_body id info_hdr mesg) - | Notice -> msgnl_with ft mesg - | Warning -> old_logger ?loc level mesg - | Error -> old_logger ?loc level mesg - let with_output_to_file fname func input = (* XXX FIXME: redirect std_ft *) (* let old_logger = !logger in *) |