diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-01-24 23:21:25 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-01-24 23:21:25 +0100 |
commit | e7bb95f2ac0d151cfdccea7b769413b332489cd3 (patch) | |
tree | d7292590bc3624c7d3ff7e4494364a50279170b9 /lib | |
parent | cfce4732363c7a93ffb7231335463d41c47074ea (diff) | |
parent | ac9f2b1a5789964b1d881d024912350a7506a0f9 (diff) |
Merge PR#383: fix #5244: set printing width ignored when given enough space
Diffstat (limited to 'lib')
-rw-r--r-- | lib/richpp.ml | 9 |
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"; |