diff options
Diffstat (limited to 'lib/pp_control.mli')
| -rw-r--r-- | lib/pp_control.mli | 27 |
1 files changed, 14 insertions, 13 deletions
diff --git a/lib/pp_control.mli b/lib/pp_control.mli index 03a1487bf1..6c92849a78 100644 --- a/lib/pp_control.mli +++ b/lib/pp_control.mli @@ -1,7 +1,7 @@ (* $Id$ *) -(* Parameters of pretty-printing *) +(* Parameters of pretty-printing. *) type pp_global_params = { margin : int; @@ -9,30 +9,31 @@ type pp_global_params = { max_depth : int; ellipsis : string } -val dflt_gp : pp_global_params (* default parameters *) -val deep_gp : pp_global_params (* with depth = 10000 *) +val dflt_gp : pp_global_params +val deep_gp : pp_global_params val set_gp : Format.formatter -> pp_global_params -> unit val set_dflt_gp : Format.formatter -> unit val get_gp : Format.formatter -> pp_global_params -(* Output functions of pretty-printing *) +(*s Output functions of pretty-printing. *) -type 'a pp_formatter_params ={ - fp_output : out_channel ; - fp_output_function : string -> int -> int -> unit ; +type 'a pp_formatter_params = { + fp_output : out_channel; + fp_output_function : string -> int -> int -> unit; fp_flush_function : unit -> unit } -val std_fp : (int*string) pp_formatter_params (* output functions for stdout *) -val err_fp : (int*string) pp_formatter_params (* output functions for stderr *) +val std_fp : (int*string) pp_formatter_params +val err_fp : (int*string) pp_formatter_params val with_fp : 'a pp_formatter_params -> Format.formatter val with_output_to : out_channel -> Format.formatter -val std_ft : Format.formatter (* the formatter on stdout *) -val err_ft : Format.formatter (* the formatter on stderr *) -val deep_ft : Format.formatter (* a deep formatter on stdout (depth=10000) *) +val std_ft : Format.formatter +val err_ft : Format.formatter +val deep_ft : Format.formatter + +(*s For parametrization through vernacular. *) -(* For parametrization through vernacular *) val set_depth_boxes : int -> unit val get_depth_boxes : unit -> int |