diff options
| author | filliatr | 1999-08-30 07:27:52 +0000 |
|---|---|---|
| committer | filliatr | 1999-08-30 07:27:52 +0000 |
| commit | 19d21ec59b69a7bd5a8e4e77794e85fed6b48d39 (patch) | |
| tree | 4d6a784866d8b8da5a8c4378b3ce3fdf9d159186 /lib/pp_control.mli | |
| parent | 72681a66688b1b81309582cfaf979a7096a118c2 (diff) | |
un petit effort de presentation dans les interfaces
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@31 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |