diff options
| author | Maxime Dénès | 2017-04-19 08:55:48 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-19 08:55:48 +0200 |
| commit | 37db2ee2d7d626fd5714a4bcf1adeb0ee9868f91 (patch) | |
| tree | b39c82573e314190d164041576206871d8600c5c | |
| parent | beb3acd2fd3831404f0be2da61d3f28e210e8349 (diff) | |
| parent | fb4d7b0cf48e2be82b9975492b23fbd46e2087ad (diff) | |
Merge PR#571: [toplevel] Fix #5475
| -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 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) |