aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-02-01 10:52:28 +0100
committerPierre-Marie Pédrot2017-02-01 10:54:53 +0100
commitc17c3faee20251cd5c7168246e9ffcd12d557f85 (patch)
tree02635866b73d7595fad009cc17535a6bbf06c2fc /lib
parentf86bfa39cddfb9c6411ed8624cee9a2b5c8d53bd (diff)
parent568b38e1d599f8bac5adf140f5a114f2871bc436 (diff)
Merge branch 'v8.6'
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";