diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /lib/pp_control.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'lib/pp_control.ml')
-rw-r--r-- | lib/pp_control.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 7aa05975..ecc54649 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pp_control.ml 10917 2008-05-10 16:35:46Z herbelin $ *) +(* $Id$ *) (* Parameters of pretty-printing *) @@ -18,7 +18,7 @@ type pp_global_params = { (* Default parameters of pretty-printing *) -let dflt_gp = { +let dflt_gp = { margin = 78; max_indent = 50; max_depth = 50; @@ -26,7 +26,7 @@ let dflt_gp = { (* A deeper pretty-printer to print proof scripts *) -let deep_gp = { +let deep_gp = { margin = 78; max_indent = 50; max_depth = 10000; @@ -35,13 +35,13 @@ let deep_gp = { (* set_gp : Format.formatter -> pp_global_params -> unit * set the parameters of a formatter *) -let set_gp ft gp = +let set_gp ft gp = Format.pp_set_margin ft gp.margin ; Format.pp_set_max_indent ft gp.max_indent ; Format.pp_set_max_boxes ft gp.max_depth ; Format.pp_set_ellipsis_text ft gp.ellipsis -let set_dflt_gp ft = set_gp ft dflt_gp +let set_dflt_gp ft = set_gp ft dflt_gp let get_gp ft = { margin = Format.pp_get_margin ft (); @@ -56,7 +56,7 @@ type 'a pp_formatter_params = { fp_output : out_channel ; fp_output_function : string -> int -> int -> unit ; fp_flush_function : unit -> unit } - + (* Output functions for stdout and stderr *) let std_fp = { @@ -69,7 +69,7 @@ let err_fp = { fp_output_function = output stderr; fp_flush_function = (fun () -> flush stderr) } -(* with_fp : 'a pp_formatter_params -> Format.formatter +(* with_fp : 'a pp_formatter_params -> Format.formatter * returns of formatter for given formatter functions *) let with_fp fp = @@ -83,7 +83,7 @@ let with_output_to ch = let ft = with_fp { fp_output = ch ; fp_output_function = (output ch) ; fp_flush_function = (fun () -> flush ch) } in - set_gp ft deep_gp; + set_gp ft deep_gp; ft let std_ft = ref Format.std_formatter @@ -105,5 +105,7 @@ let set_depth_boxes v = let get_margin () = Some (Format.pp_get_margin !std_ft ()) let set_margin v = - Format.pp_set_margin !std_ft (match v with None -> default_margin | Some v -> v) + let v = match v with None -> default_margin | Some v -> v in + Format.pp_set_margin !std_ft v; + Format.pp_set_margin !deep_ft v |