diff options
| author | Emilio Jesus Gallego Arias | 2016-02-11 02:13:30 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-04-18 10:31:28 +0200 |
| commit | aa99eef44dfa439a7c62b29f1a6c39525dc82acf (patch) | |
| tree | 12ca7fa66464dbdbf7e89b40a74f3a21d70503a4 /plugins | |
| parent | d926105c022177b70578982d037b12e5d914922b (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.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions
