diff options
Diffstat (limited to 'vernac/topfmt.mli')
| -rw-r--r-- | vernac/topfmt.mli | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 909dd7077..6c8e0ae2f 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -36,19 +36,22 @@ val get_depth_boxes : unit -> int option val set_margin : int option -> unit val get_margin : unit -> int option -(** Headers for tagging *) -val err_hdr : Pp.std_ppcmds -val ann_hdr : Pp.std_ppcmds - (** Console display of feedback, we may add some location information *) val std_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit +(** Color output *) val init_color_output : unit -> unit val clear_styles : unit -> unit val parse_color_config : string -> unit val dump_tags : unit -> (string * Terminal.style) list +(** Error printing *) +(* To be deprecated when we can fully move to feedback-based error + printing. *) +val pr_loc : Loc.t -> Pp.std_ppcmds +val print_err_exn : ?extra:Pp.std_ppcmds -> exn -> unit + (** [with_output_to_file file f x] executes [f x] with logging redirected to a file [file] *) val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b |