From aa99eef44dfa439a7c62b29f1a6c39525dc82acf Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 11 Feb 2016 02:13:30 +0100
Subject: [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.
---
 lib/pp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/pp.ml b/lib/pp.ml
index 4f50e3e19b..3fcb6ac595 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 ->
-- 
cgit v1.2.3