aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-01-24 23:21:25 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-01-24 23:21:25 +0100
commite7bb95f2ac0d151cfdccea7b769413b332489cd3 (patch)
treed7292590bc3624c7d3ff7e4494364a50279170b9 /lib
parentcfce4732363c7a93ffb7231335463d41c47074ea (diff)
parentac9f2b1a5789964b1d881d024912350a7506a0f9 (diff)
Merge PR#383: fix #5244: set printing width ignored when given enough space
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 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 <pp> tags. *)
pp_open_tag ft "pp";