diff options
| -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"; |