From 3fc02bb2034a648c9c27b76a9e7b4e02a78e55b9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 5 Dec 2016 17:56:22 +0100 Subject: [pp] Move terminal-specific tagging to the toplevel. Previously, tags were associated to terminal styles, which doesn't make sense on terminal-free pretty printing scenarios. This commit moves tag interpretation to the toplevel terminal handling module `Topfmt`. --- vernac/topfmt.mli | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'vernac/topfmt.mli') diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 38a400cfd..1555f80a9 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -36,12 +36,18 @@ 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 + (** Console display of feedback *) val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit 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 (** [with_output_to_file file f x] executes [f x] with logging redirected to a file [file] *) -- cgit v1.2.3