aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-02-11 02:13:30 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-04-18 10:31:28 +0200
commitaa99eef44dfa439a7c62b29f1a6c39525dc82acf (patch)
tree12ca7fa66464dbdbf7e89b40a74f3a21d70503a4
parentd926105c022177b70578982d037b12e5d914922b (diff)
[pp] Ensure Format is called with top level boxes.
The documentation of Ocaml's `Format` module specifies: > The behaviour of pretty-printing commands is unspecified if there is > no opened pretty-printing box. Each box opened via one of the open_ > functions below must be closed using close_box for proper > formatting. Otherwise, some of the material printed in the boxes may > not be output, or may be formatted incorrectly. (http://caml.inria.fr/pub/docs/manual-ocaml/libref/Format.html) However, [lib/pp.ml] seems not to take lots of precautions to ensure that format is always called with an enclosing box. If `log_via_feedback` is set, [lib/pp.ml:string_of_ppcmds] will call `msg_with` without a top-level enclosing box, resulting in poor display results like mismatched width. Note that there are more functions affected, but these codepaths don't seem to matter when `log_via_feedback` is set. A small cleanup of pp.ml may be in order.
-rw-r--r--lib/pp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index 4f50e3e19..3fcb6ac59 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -508,7 +508,7 @@ let get_id_for_feedback () = !feedback_id, !feedback_route
(** Utility *)
let string_of_ppcmds c =
- msg_with Format.str_formatter c;
+ Format.fprintf Format.str_formatter "@[%a@]" msg_with c;
Format.flush_str_formatter ()
let log_via_feedback () = logger := (fun ~id lvl msg ->