diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /lib/pp_control.ml | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'lib/pp_control.ml')
-rw-r--r-- | lib/pp_control.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 0d224c03..969c1550 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -20,7 +20,7 @@ let dflt_gp = { margin = 78; max_indent = 50; max_depth = 50; - ellipsis = ".." } + ellipsis = "..." } (* A deeper pretty-printer to print proof scripts *) @@ -84,5 +84,10 @@ let set_margin v = let v = match v with None -> default_margin | Some v -> v in Format.pp_set_margin Format.str_formatter v; Format.pp_set_margin !std_ft v; - Format.pp_set_margin !deep_ft v - + Format.pp_set_margin !deep_ft v; + (* Heuristic, based on usage: the column on the right of max_indent + column is 20% of width, capped to 30 characters *) + let m = max (64 * v / 100) (v-30) in + Format.pp_set_max_indent Format.str_formatter m; + Format.pp_set_max_indent !std_ft m; + Format.pp_set_max_indent !deep_ft m |