aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2016-12-04 11:40:36 +0100
committerEmilio Jesus Gallego Arias2016-12-04 22:57:51 +0100
commitac9f2b1a5789964b1d881d024912350a7506a0f9 (patch)
tree5d9d6a9ded48c3505150f4977b1b8c1f1f924023 /lib
parentf653036a73f008168809d3f50041382fe3ee52a1 (diff)
[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.
Diffstat (limited to 'lib')
-rw-r--r--lib/richpp.ml9
1 files changed, 8 insertions, 1 deletions
diff --git a/lib/richpp.ml b/lib/richpp.ml
index a98273edb2..d1c6d158e4 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 <pp> tags. *)
pp_open_tag ft "pp";