From fb4d7b0cf48e2be82b9975492b23fbd46e2087ad Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 18 Apr 2017 22:59:28 +0200 Subject: [toplevel] Fix #5475 This was a logic error in 63cfc77ddf3586262d905dc351b58669d185a55e, `Notice`-level messages should not be wrapped in `` tags. --- vernac/topfmt.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index ee55366927..a4acd3f24e 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -141,11 +141,13 @@ let ann_hdr = tag Tag.error (str "Anomaly:") ++ spc () let make_body quoter info ?pre_hdr s = pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s)) +(* The empty quoter *) +let noq x = x (* Generic logger *) let gen_logger dbg err ?pre_hdr level msg = 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 dbg info_hdr ?pre_hdr msg) + | Notice -> msgnl_with !std_ft (make_body noq info_hdr ?pre_hdr msg) | Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (make_body err warn_hdr ?pre_hdr msg)) () | Error -> msgnl_with !err_ft (make_body err err_hdr ?pre_hdr msg) -- cgit v1.2.3