diff options
| author | glondu | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /lib/pp_control.ml | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/pp_control.ml')
| -rw-r--r-- | lib/pp_control.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 7617d5ca42..ecc546491d 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -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 |