From ac9f2b1a5789964b1d881d024912350a7506a0f9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 4 Dec 2016 11:40:36 +0100 Subject: [pp] Set printing width for richpp formatter (bug #5244) Richpp output depends on printing width, thus its internal formatter should be seeded with the proper width value. While we are at it, we increase the default buffer size to a more sensible value. --- lib/richpp.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'lib/richpp.ml') diff --git a/lib/richpp.ml b/lib/richpp.ml index a98273edb..d1c6d158e 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -55,7 +55,7 @@ let rich_pp annotate ppcmds = string_of_int index in - let pp_buffer = Buffer.create 13 in + let pp_buffer = Buffer.create 180 in let push_pcdata () = (** Push the optional PCData on the above node *) @@ -113,6 +113,13 @@ let rich_pp annotate ppcmds = pp_set_formatter_tag_functions ft tag_functions; pp_set_mark_tags ft true; + (* Set formatter width. This is currently a hack and duplicate code + with Pp_control. Hopefully it will be fixed better in Coq 8.7 *) + let w = pp_get_margin str_formatter () in + let m = max (64 * w / 100) (w-30) in + pp_set_margin ft w; + pp_set_max_indent ft m; + (** The whole output must be a valid document. To that end, we nest the document inside tags. *) pp_open_tag ft "pp"; -- cgit v1.2.3