From a8ec2dc5c330ded1ba400ef202c57e68d2533312 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 5 Dec 2016 18:17:46 +0100 Subject: [pp] Remove special tag type and handler from Pp. For legacy reasons, pretty printing required to provide a "tag" interpretation function `pp_tag`. However such function was not of much use as the backends (richpp and terminal) hooked at the `Format.tag` level. We thus remove this unused indirection layer and annotate expressions with their `Format` tags. This is a step towards moving the last bit of terminal code out of the core system. --- vernac/topfmt.ml | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) (limited to 'vernac/topfmt.ml') diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 85981c386..e5063e27b 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -99,8 +99,8 @@ let set_margin v = type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit -let msgnl_with ?pp_tag fmt strm = - pp_with ?pp_tag fmt (strm ++ fnl ()); +let msgnl_with fmt strm = + pp_with fmt (strm ++ fnl ()); Format.pp_print_flush fmt () (* XXX: This is really painful! *) @@ -133,25 +133,24 @@ let make_body quoter info ?loc s = quoter (hov 0 (loc ++ info ++ s)) (* Generic logger *) -let gen_logger ?pp_tag dbg err ?loc level msg = match level with - | Debug -> msgnl_with ?pp_tag !std_ft (make_body dbg dbg_str ?loc msg) - | Info -> msgnl_with ?pp_tag !std_ft (make_body dbg info_str ?loc msg) +let gen_logger dbg err ?loc level msg = match level with + | Debug -> msgnl_with !std_ft (make_body dbg dbg_str ?loc msg) + | Info -> msgnl_with !std_ft (make_body dbg info_str ?loc msg) (* XXX: What to do with loc here? *) - | Notice -> msgnl_with ?pp_tag !std_ft msg + | Notice -> msgnl_with !std_ft msg | Warning -> Flags.if_warn (fun () -> - msgnl_with ?pp_tag !err_ft (make_body err warn_str ?loc msg)) () - | Error -> msgnl_with ?pp_tag !err_ft (make_body err err_str ?loc msg) + msgnl_with !err_ft (make_body err warn_str ?loc msg)) () + | Error -> msgnl_with !err_ft (make_body err err_str ?loc msg) (** Standard loggers *) (* We provide a generic clear_log_backend callback for backends wanting to do clenaup after the print. *) -let std_logger_tag = ref None let std_logger_cleanup = ref (fun () -> ()) let std_logger ?loc level msg = - gen_logger (fun x -> x) (fun x -> x) ?pp_tag:!std_logger_tag ?loc level msg; + gen_logger (fun x -> x) (fun x -> x) ?loc level msg; !std_logger_cleanup () (** Color logging. Moved from pp_style, it may need some more refactoring *) @@ -176,7 +175,7 @@ let make_style_stack () = | st :: _ -> st in let push tag = - let style = match Ppstyle.get_style_format tag with + let style = match Ppstyle.get_style tag with | None -> empty | Some st -> st in @@ -199,7 +198,6 @@ let make_style_stack () = let init_color_output () = let push_tag, pop_tag, clear_tag = make_style_stack () in std_logger_cleanup := clear_tag; - std_logger_tag := Some Ppstyle.to_format; let tag_handler = { Format.mark_open_tag = push_tag; Format.mark_close_tag = pop_tag; -- cgit v1.2.3