diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-18 22:59:28 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-18 22:59:28 +0200 |
| commit | fb4d7b0cf48e2be82b9975492b23fbd46e2087ad (patch) | |
| tree | b39c82573e314190d164041576206871d8600c5c /vernac/topfmt.ml | |
| parent | beb3acd2fd3831404f0be2da61d3f28e210e8349 (diff) | |
[toplevel] Fix #5475
This was a logic error in 63cfc77ddf3586262d905dc351b58669d185a55e,
`Notice`-level messages should not be wrapped in `<infomsg>` tags.
Diffstat (limited to 'vernac/topfmt.ml')
| -rw-r--r-- | vernac/topfmt.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index ee5536692..a4acd3f24 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) |