1995-08-09 08:06:35 -07:00
|
|
|
(***********************************************************************)
|
|
|
|
(* *)
|
1996-04-30 07:53:58 -07:00
|
|
|
(* Objective Caml *)
|
1995-08-09 08:06:35 -07:00
|
|
|
(* *)
|
1997-10-23 00:53:12 -07:00
|
|
|
(* Pierre Weis, projet Cristal, INRIA Rocquencourt *)
|
1995-08-09 08:06:35 -07:00
|
|
|
(* *)
|
1996-04-30 07:53:58 -07:00
|
|
|
(* Copyright 1996 Institut National de Recherche en Informatique et *)
|
1999-11-17 10:59:06 -08:00
|
|
|
(* en Automatique. All rights reserved. This file is distributed *)
|
2001-12-07 05:41:02 -08:00
|
|
|
(* under the terms of the GNU Library General Public License, with *)
|
|
|
|
(* the special exception on linking described in file ../LICENSE. *)
|
1995-08-09 08:06:35 -07:00
|
|
|
(* *)
|
|
|
|
(***********************************************************************)
|
|
|
|
|
|
|
|
(* $Id$ *)
|
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
(** Pretty printing.
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
This module implements a pretty-printing facility to format text
|
1995-05-04 03:15:53 -07:00
|
|
|
within ``pretty-printing boxes''. The pretty-printer breaks lines
|
1996-07-08 11:53:26 -07:00
|
|
|
at specified break hints, and indents lines according to the box
|
2001-06-12 08:25:04 -07:00
|
|
|
structure.
|
|
|
|
|
|
|
|
Warning: the material output by the following functions is delayed
|
|
|
|
in the pretty-printer queue in order to compute the proper line
|
|
|
|
breaking. Hence, you should not mix calls to the printing functions
|
|
|
|
of the basic I/O system with calls to the functions of this module:
|
|
|
|
this could result in some strange output seemingly unrelated with
|
2001-10-26 15:37:14 -07:00
|
|
|
the evaluation order of printing commands.
|
|
|
|
|
|
|
|
You may consider this module as providing an extension to the
|
1998-12-08 00:29:54 -08:00
|
|
|
[printf] facility to provide automatic line breaking. The addition of
|
1999-02-23 10:00:17 -08:00
|
|
|
pretty-printing annotations to your regular [printf] formats gives you
|
1998-12-08 00:29:54 -08:00
|
|
|
fancy indentation and line breaks.
|
|
|
|
Pretty-printing annotations are described below in the documentation of
|
2001-10-26 15:37:14 -07:00
|
|
|
the function {!Format.fprintf}.
|
|
|
|
|
1998-12-08 00:29:54 -08:00
|
|
|
You may also use the explicit box management and printing functions
|
|
|
|
provided by this module. This style is more basic but more verbose
|
2001-10-31 03:04:35 -08:00
|
|
|
than the [fprintf] concise formats.
|
1998-12-08 00:29:54 -08:00
|
|
|
|
|
|
|
For instance, the sequence
|
2003-07-05 04:13:24 -07:00
|
|
|
[open_box 0; print_string "x ="; print_space (); print_int 1; close_box ()]
|
1998-12-08 00:29:54 -08:00
|
|
|
that prints [x = 1] within a pretty-printing box, can be
|
2002-01-20 09:38:52 -08:00
|
|
|
abbreviated as [printf "@[%s@ %i@]" "x =" 1], or even shorter
|
|
|
|
[printf "@[x =@ %i@]" 1].
|
1998-12-08 00:29:54 -08:00
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
Rule of thumb for casual users of this library:
|
2002-05-27 00:04:48 -07:00
|
|
|
- use simple boxes (as obtained by [open_box 0]);
|
|
|
|
- use simple break hints (as obtained by [print_cut ()] that outputs a
|
1998-04-27 02:55:50 -07:00
|
|
|
simple break hint, or by [print_space ()] that outputs a space
|
1997-02-26 07:02:26 -08:00
|
|
|
indicating a break hint);
|
2002-05-27 00:04:48 -07:00
|
|
|
- once a box is opened, display its material with basic printing
|
1996-07-08 11:53:26 -07:00
|
|
|
functions (e. g. [print_int] and [print_string]);
|
2002-05-27 00:04:48 -07:00
|
|
|
- when the material for a box has been printed, call [close_box ()] to
|
1996-07-08 11:53:26 -07:00
|
|
|
close the box;
|
2002-05-27 00:04:48 -07:00
|
|
|
- at the end of your routine, evaluate [print_newline ()] to close
|
2001-10-26 15:37:14 -07:00
|
|
|
all remaining boxes and flush the pretty-printer.
|
|
|
|
|
|
|
|
The behaviour of pretty-printing commands is unspecified
|
1996-07-08 11:53:26 -07:00
|
|
|
if there is no opened pretty-printing box. Each box opened via
|
|
|
|
one of the [open_] functions below must be closed using [close_box]
|
|
|
|
for proper formatting. Otherwise, some of the material printed in the
|
2001-10-26 15:37:14 -07:00
|
|
|
boxes may not be output, or may be formatted incorrectly.
|
|
|
|
|
|
|
|
In case of interactive use, the system closes all opened boxes and
|
1996-07-08 11:53:26 -07:00
|
|
|
flushes all pending text (as with the [print_newline] function)
|
|
|
|
after each phrase. Each phrase is therefore executed in the initial
|
2001-10-26 15:37:14 -07:00
|
|
|
state of the pretty-printer.
|
|
|
|
*)
|
|
|
|
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 Boxes} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val open_box : int -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [open_box d] opens a new pretty-printing box
|
|
|
|
with offset [d].
|
|
|
|
This box is the general purpose pretty-printing box.
|
|
|
|
Material in this box is displayed ``horizontal or vertical'':
|
|
|
|
break hints inside the box may lead to a new line, if there
|
|
|
|
is no more room on the line to print the remainder of the box,
|
|
|
|
or if a new line may lead to a new indentation
|
|
|
|
(demonstrating the indentation of the box).
|
|
|
|
When a new line is printed in the box, [d] is added to the
|
|
|
|
current indentation. *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val close_box : unit -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Closes the most recently opened pretty-printing box. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 Formatting functions} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_string : string -> unit;;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** [print_string str] prints [str] in the current box. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_as : int -> string -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [print_as len str] prints [str] in the
|
|
|
|
current box. The pretty-printer formats [str] as if
|
|
|
|
it were of length [len]. *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_int : int -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Prints an integer in the current box. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_float : float -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Prints a floating point number in the current box. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_char : char -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Prints a character in the current box. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_bool : bool -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Prints a boolean in the current box. *)
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 Break hints} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_space : unit -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [print_space ()] is used to separate items (typically to print
|
|
|
|
a space between two words).
|
|
|
|
It indicates that the line may be split at this
|
|
|
|
point. It either prints one space or splits the line.
|
2001-10-31 03:04:35 -08:00
|
|
|
It is equivalent to [print_break 1 0]. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_cut : unit -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [print_cut ()] is used to mark a good break position.
|
|
|
|
It indicates that the line may be split at this
|
|
|
|
point. It either prints nothing or splits the line.
|
|
|
|
This allows line splitting at the current
|
|
|
|
point, without printing spaces or adding indentation.
|
2001-10-31 03:04:35 -08:00
|
|
|
It is equivalent to [print_break 0 0]. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_break : int -> int -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Inserts a break hint in a pretty-printing box.
|
2001-10-26 15:37:14 -07:00
|
|
|
[print_break nspaces offset] indicates that the line may
|
|
|
|
be split (a newline character is printed) at this point,
|
|
|
|
if the contents of the current box does not fit on the
|
|
|
|
current line.
|
|
|
|
If the line is split at that point, [offset] is added to
|
|
|
|
the current indentation. If the line is not split,
|
|
|
|
[nspaces] spaces are printed. *)
|
1997-05-15 03:41:17 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_flush : unit -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Flushes the pretty printer: all opened boxes are closed,
|
2001-10-26 15:37:14 -07:00
|
|
|
and all pending text is displayed. *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_newline : unit -> unit;;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** Equivalent to [print_flush] followed by a new line. *)
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val force_newline : unit -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Forces a newline in the current box. Not the normal way of
|
2001-10-26 15:37:14 -07:00
|
|
|
pretty-printing, you should prefer break hints. *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_if_newline : unit -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Executes the next formatting command if the preceding line
|
2001-10-26 15:37:14 -07:00
|
|
|
has just been split. Otherwise, ignore the next formatting
|
|
|
|
command. *)
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 Margin} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val set_margin : int -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [set_margin d] sets the value of the right margin
|
|
|
|
to [d] (in characters): this value is used to detect line
|
|
|
|
overflows that leads to split lines.
|
|
|
|
Nothing happens if [d] is smaller than 2 or
|
|
|
|
bigger than 999999999. *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val get_margin : unit -> int;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Returns the position of the right margin. *)
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 Maximum indentation limit} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val set_max_indent : int -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [set_max_indent d] sets the value of the maximum
|
|
|
|
indentation limit to [d] (in characters):
|
|
|
|
once this limit is reached, boxes are rejected to the left,
|
|
|
|
if they do not fit on the current line.
|
|
|
|
Nothing happens if [d] is smaller than 2 or
|
|
|
|
bigger than 999999999. *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val get_max_indent : unit -> int;;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** Return the value of the maximum indentation limit (in characters). *)
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 Formatting depth: maximum number of boxes allowed before ellipsis} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val set_max_boxes : int -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [set_max_boxes max] sets the maximum number
|
|
|
|
of boxes simultaneously opened.
|
|
|
|
Material inside boxes nested deeper is printed as an
|
|
|
|
ellipsis (more precisely as the text returned by
|
2001-10-31 03:04:35 -08:00
|
|
|
[get_ellipsis_text ()]).
|
2001-10-26 15:37:14 -07:00
|
|
|
Nothing happens if [max] is not greater than 1. *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val get_max_boxes : unit -> int;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Returns the maximum number of boxes allowed before ellipsis. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val over_max_boxes : unit -> bool;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Tests if the maximum number of boxes allowed have already been opened. *)
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 Advanced formatting} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val open_hbox : unit -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [open_hbox ()] opens a new pretty-printing box.
|
|
|
|
This box is ``horizontal'': the line is not split in this box
|
|
|
|
(new lines may still occur inside boxes nested deeper). *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val open_vbox : int -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [open_vbox d] opens a new pretty-printing box
|
|
|
|
with offset [d].
|
|
|
|
This box is ``vertical'': every break hint inside this
|
|
|
|
box leads to a new line.
|
|
|
|
When a new line is printed in the box, [d] is added to the
|
|
|
|
current indentation. *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val open_hvbox : int -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [open_hvbox d] opens a new pretty-printing box
|
|
|
|
with offset [d].
|
|
|
|
This box is ``horizontal-vertical'': it behaves as an
|
|
|
|
``horizontal'' box if it fits on a single line,
|
|
|
|
otherwise it behaves as a ``vertical'' box.
|
|
|
|
When a new line is printed in the box, [d] is added to the
|
|
|
|
current indentation. *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val open_hovbox : int -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [open_hovbox d] opens a new pretty-printing box
|
|
|
|
with offset [d].
|
|
|
|
This box is ``horizontal or vertical'': break hints
|
|
|
|
inside this box may lead to a new line, if there is no more room
|
|
|
|
on the line to print the remainder of the box.
|
|
|
|
When a new line is printed in the box, [d] is added to the
|
|
|
|
current indentation. *)
|
|
|
|
|
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 Tabulations} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val open_tbox : unit -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Opens a tabulation box. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val close_tbox : unit -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Closes the most recently opened tabulation box. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_tbreak : int -> int -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** Break hint in a tabulation box.
|
|
|
|
[print_tbreak spaces offset] moves the insertion point to
|
|
|
|
the next tabulation ([spaces] being added to this position).
|
|
|
|
Nothing occurs if insertion point is already on a
|
|
|
|
tabulation mark.
|
|
|
|
If there is no next tabulation on the line, then a newline
|
|
|
|
is printed and the insertion point moves to the first
|
|
|
|
tabulation of the box.
|
|
|
|
If a new line is printed, [offset] is added to the current
|
|
|
|
indentation. *)
|
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val set_tab : unit -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Sets a tabulation mark at the current insertion point. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val print_tab : unit -> unit;;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** [print_tab ()] is equivalent to [print_tbreak (0,0)]. *)
|
1997-05-13 11:27:27 -07:00
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-05-08 06:50:29 -07:00
|
|
|
(** {6 Ellipsis} *)
|
|
|
|
|
|
|
|
val set_ellipsis_text : string -> unit;;
|
|
|
|
(** Set the text of the ellipsis printed when too many boxes
|
|
|
|
are opened (a single dot, [.], by default). *)
|
|
|
|
|
|
|
|
val get_ellipsis_text : unit -> string;;
|
|
|
|
(** Return the text of the ellipsis. *)
|
|
|
|
|
|
|
|
|
2002-03-11 14:18:20 -08:00
|
|
|
(** {6 Tags} *)
|
|
|
|
|
2002-05-08 06:50:29 -07:00
|
|
|
type tag = string;;
|
2002-03-11 14:18:20 -08:00
|
|
|
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Tags are used to decorate printed entities for user's defined
|
2002-03-11 14:18:20 -08:00
|
|
|
purposes, e.g. setting font and giving size indications for a
|
|
|
|
display device, or marking delimitations of semantics entities
|
2002-03-19 22:51:17 -08:00
|
|
|
(e.g. HTML or TeX elements or terminal escape sequences).
|
2002-03-11 14:18:20 -08:00
|
|
|
|
2002-05-08 06:50:29 -07:00
|
|
|
By default, those tags do not influence line breaking calculation:
|
|
|
|
the tag ``markers'' are not considered as part of the printing
|
|
|
|
material that drive line breaking (in other words, the length of
|
|
|
|
those strings is considered as zero for line breaking).
|
|
|
|
|
|
|
|
Thus, tag handling is in some sense transparent to pretty-printing
|
2003-09-25 00:43:54 -07:00
|
|
|
and does not interfere with usual pretty-printing. Hence, a single
|
2002-05-08 06:50:29 -07:00
|
|
|
pretty printing routine can output both simple ``verbatim''
|
|
|
|
material or richer decorated output depending on the treatment of
|
2003-09-25 00:43:54 -07:00
|
|
|
tags. By default, tags are not active, hence the output is not
|
|
|
|
decorated with tag information. Once [set_tags] is set to [true],
|
|
|
|
the pretty printer engine honors tags and decorates the output
|
|
|
|
accordingly.
|
2002-05-08 06:50:29 -07:00
|
|
|
|
|
|
|
When a tag has been opened (or closed), it is both and successively
|
|
|
|
``printed'' and ``marked''. Printing a tag means calling a
|
|
|
|
formatter specific function with the name of the tag as argument:
|
|
|
|
that ``tag printing'' function can then print any regular material
|
|
|
|
to the formatter (so that this material is enqueued as usual in the
|
|
|
|
formatter queue for further line-breaking computation). Marking a
|
|
|
|
tag means to output an arbitrary string (the ``tag marker''),
|
|
|
|
directly into the output device of the formatter. Hence, the
|
|
|
|
formatter specific ``tag marking'' function must return the tag
|
|
|
|
marker string associated to its tag argument. Being flushed
|
|
|
|
directly into the output device of the formatter, tag marker
|
|
|
|
strings are not considered as part of the printing material that
|
|
|
|
drive line breaking (in other words, the length of the strings
|
|
|
|
corresponding to tag markers is considered as zero for line
|
|
|
|
breaking). In addition, advanced users may take advantage of
|
|
|
|
the specificity of tag markers to be precisely output when the
|
|
|
|
pretty printer has already decided where to break the lines, and
|
|
|
|
precisely when the queue is flushed into the output device.
|
|
|
|
|
|
|
|
In the spirit of HTML tags, the default tag marking functions
|
|
|
|
output tags enclosed in "<" and ">": hence, the opening marker of
|
|
|
|
tag [t] is ["<t>"] and the closing marker ["</t>"].
|
|
|
|
|
|
|
|
Default tag printing functions just do nothing.
|
|
|
|
|
|
|
|
Tag marking and tag printing functions are user definable and can
|
|
|
|
be set by calling [set_formatter_tag_functions]. *)
|
2002-03-11 14:18:20 -08:00
|
|
|
|
2002-03-19 22:51:17 -08:00
|
|
|
val open_tag : tag -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** [open_tag t] opens the tag named [t]; the [print_open_tag]
|
|
|
|
function of the formatter is called with [t] as argument;
|
|
|
|
the tag marker [mark_open_tag t] will be flushed into the output
|
|
|
|
device of the formatter. *)
|
2002-03-11 14:18:20 -08:00
|
|
|
val close_tag : unit -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** [close_tag ()] closes the most recently opened tag [t].
|
|
|
|
In addition, the [print_close_tag] function of the formatter is called
|
|
|
|
with [t] as argument. The marker [mark_close_tag t] will be flushed
|
|
|
|
into the output device of the formatter. *)
|
2002-03-11 14:18:20 -08:00
|
|
|
|
2002-05-08 06:50:29 -07:00
|
|
|
val set_tags : bool -> unit;;
|
2003-01-24 06:26:56 -08:00
|
|
|
(** [set_tags b] turns on or off the treatment of tags (default is off). *)
|
2002-03-19 22:51:17 -08:00
|
|
|
val set_print_tags : bool -> unit;;
|
2002-03-19 23:33:20 -08:00
|
|
|
val set_mark_tags : bool -> unit;;
|
2003-01-24 06:26:56 -08:00
|
|
|
(** [set_print_tags b] turns on or off the printing of tags, while
|
2002-05-08 06:50:29 -07:00
|
|
|
[set_mark_tags b] turns on or off the output of tag markers. *)
|
2002-03-22 12:43:07 -08:00
|
|
|
val get_print_tags : unit -> bool;;
|
|
|
|
val get_mark_tags : unit -> bool;;
|
|
|
|
(** Return the current status of tag printing and marking. *)
|
2002-03-11 14:18:20 -08:00
|
|
|
|
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 Redirecting formatter output} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val set_formatter_out_channel : out_channel -> unit;;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** Redirect the pretty-printer output to the given channel. *)
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2001-11-04 13:25:23 -08:00
|
|
|
val set_formatter_output_functions :
|
2002-03-05 12:56:46 -08:00
|
|
|
(string -> int -> int -> unit) -> (unit -> unit) -> unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [set_formatter_output_functions out flush] redirects the
|
|
|
|
pretty-printer output to the functions [out] and [flush].
|
2002-03-05 12:56:46 -08:00
|
|
|
|
|
|
|
The [out] function performs the pretty-printer output. It is called
|
|
|
|
with a string [s], a start position [p], and a number of characters
|
|
|
|
[n]; it is supposed to output characters [p] to [p + n - 1] of
|
|
|
|
[s]. The [flush] function is called whenever the pretty-printer is
|
|
|
|
flushed using [print_flush] or [print_newline]. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
val get_formatter_output_functions :
|
2002-03-05 12:56:46 -08:00
|
|
|
unit -> (string -> int -> int -> unit) * (unit -> unit);;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** Return the current output functions of the pretty-printer. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-05-08 06:50:29 -07:00
|
|
|
(** {6 Changing the meaning of printing tags} *)
|
2002-03-11 14:18:20 -08:00
|
|
|
|
2002-05-08 06:50:29 -07:00
|
|
|
type formatter_tag_functions = {
|
|
|
|
mark_open_tag : tag -> string;
|
|
|
|
mark_close_tag : tag -> string;
|
|
|
|
print_open_tag : tag -> unit;
|
|
|
|
print_close_tag : tag -> unit;
|
|
|
|
};;
|
|
|
|
(** The tag handling functions specific to a formatter:
|
|
|
|
[mark] versions are the ``tag marking'' functions that associate a string
|
|
|
|
marker to a tag in order for the pretty-printing engine to flush
|
|
|
|
those markers as 0 length tokens in the output device of the formatter.
|
|
|
|
[print] versions are the ``tag printing'' functions that can perform
|
|
|
|
regular printing when a tag is closed or opened. *)
|
|
|
|
|
|
|
|
val set_formatter_tag_functions :
|
|
|
|
formatter_tag_functions -> unit;;
|
|
|
|
|
|
|
|
(** [set_formatter_tag_functions tag_funs] changes the meaning of
|
|
|
|
opening and closing tags to use the functions in [tag_funs].
|
|
|
|
|
|
|
|
When opening a tag name [t], the string [t] is passed to the
|
|
|
|
opening tag marking function (the [mark_open_tag] field of the
|
2002-05-27 00:04:48 -07:00
|
|
|
record [tag_funs]), that must return the opening tag marker for
|
2002-05-08 06:50:29 -07:00
|
|
|
that name. When the next call to [close_tag ()] happens, the tag
|
|
|
|
name [t] is sent back to the closing tag marking function (the
|
|
|
|
[mark_close_tag] field of record [tag_funs]), that must return a
|
|
|
|
closing tag marker for that name.
|
|
|
|
|
|
|
|
The [print_] field of the record contains the functions that are
|
|
|
|
called at tag opening and tag closing time, to output regular
|
|
|
|
material in the pretty-printer queue. *)
|
2002-03-11 14:18:20 -08:00
|
|
|
|
|
|
|
val get_formatter_tag_functions :
|
2002-05-08 06:50:29 -07:00
|
|
|
unit -> formatter_tag_functions;;
|
2002-03-11 14:18:20 -08:00
|
|
|
(** Return the current tag functions of the pretty-printer. *)
|
2002-05-08 06:50:29 -07:00
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 Changing the meaning of pretty printing (indentation, line breaking, and printing material)} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2001-11-04 13:25:23 -08:00
|
|
|
val set_all_formatter_output_functions :
|
2002-03-05 12:56:46 -08:00
|
|
|
out:(string -> int -> int -> unit) ->
|
|
|
|
flush:(unit -> unit) ->
|
|
|
|
newline:(unit -> unit) ->
|
|
|
|
spaces:(int -> unit) ->
|
|
|
|
unit;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [set_all_formatter_output_functions out flush outnewline outspace]
|
2002-03-05 12:56:46 -08:00
|
|
|
redirects the pretty-printer output to the functions [out] and
|
|
|
|
[flush] as described in [set_formatter_output_functions]. In
|
|
|
|
addition, the pretty-printer function that outputs a newline is set
|
|
|
|
to the function [outnewline] and the function that outputs
|
|
|
|
indentation spaces is set to the function [outspace].
|
|
|
|
|
|
|
|
This way, you can change the meaning of indentation (which can be
|
|
|
|
something else than just printing space characters) and the
|
|
|
|
meaning of new lines opening (which can be connected to any other
|
|
|
|
action needed by the application at hand). The two functions
|
|
|
|
[outspace] and [outnewline] are normally connected to [out] and
|
|
|
|
[flush]: respective default values for [outspace] and [outnewline]
|
|
|
|
are [out (String.make n ' ') 0 n] and [out "\n" 0 1]. *)
|
2002-01-20 09:38:52 -08:00
|
|
|
|
2001-12-03 14:01:28 -08:00
|
|
|
val get_all_formatter_output_functions :
|
|
|
|
unit ->
|
2002-03-05 12:56:46 -08:00
|
|
|
(string -> int -> int -> unit) *
|
|
|
|
(unit -> unit) *
|
|
|
|
(unit -> unit) *
|
|
|
|
(int -> unit);;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** Return the current output functions of the pretty-printer,
|
|
|
|
including line breaking and indentation functions. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 Multiple formatted output} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
type formatter;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** Abstract data type corresponding to a pretty-printer (also called a
|
|
|
|
formatter) and all its machinery.
|
2001-10-26 15:37:14 -07:00
|
|
|
Defining new pretty-printers permits the output of
|
|
|
|
material in parallel on several channels.
|
2001-11-04 13:25:23 -08:00
|
|
|
Parameters of a pretty-printer are local to this pretty-printer:
|
2001-10-26 15:37:14 -07:00
|
|
|
margin, maximum indentation limit, maximum number of boxes
|
|
|
|
simultaneously opened, ellipsis, and so on, are specific to
|
|
|
|
each pretty-printer and may be fixed independently.
|
|
|
|
Given an output channel [oc], a new formatter writing to
|
2001-10-31 03:04:35 -08:00
|
|
|
that channel is obtained by calling [formatter_of_out_channel oc].
|
2001-11-04 13:25:23 -08:00
|
|
|
Alternatively, the [make_formatter] function allocates a new
|
2001-10-26 15:37:14 -07:00
|
|
|
formatter with explicit output and flushing functions
|
|
|
|
(convenient to output material to strings for instance). *)
|
1998-12-08 00:29:54 -08:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val formatter_of_out_channel : out_channel -> formatter;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [formatter_of_out_channel oc] returns a new formatter that
|
|
|
|
writes to the corresponding channel [oc]. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val std_formatter : formatter;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** The standard formatter used by the formatting functions
|
2001-10-31 03:04:35 -08:00
|
|
|
above. It is defined as [formatter_of_out_channel stdout]. *)
|
1997-05-15 03:41:17 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val err_formatter : formatter;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** A formatter to use with formatting functions below for
|
|
|
|
output to standard error. It is defined as
|
2002-05-08 06:50:29 -07:00
|
|
|
[formatter_of_out_channel stderr]. *)
|
1996-07-08 11:53:26 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val formatter_of_buffer : Buffer.t -> formatter;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [formatter_of_buffer b] returns a new formatter writing to
|
|
|
|
buffer [b]. As usual, the formatter has to be flushed at
|
2001-10-31 03:04:35 -08:00
|
|
|
the end of pretty printing, using [pp_print_flush] or
|
2001-11-04 13:25:23 -08:00
|
|
|
[pp_print_newline], to display all the pending material. *)
|
1999-02-16 01:07:26 -08:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val stdbuf : Buffer.t;;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** The string buffer in which [str_formatter] writes. *)
|
1999-02-16 01:07:26 -08:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val str_formatter : formatter;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** A formatter to use with formatting functions below for
|
2001-10-31 03:04:35 -08:00
|
|
|
output to the [stdbuf] string buffer.
|
2002-03-05 12:56:46 -08:00
|
|
|
[str_formatter] is defined as [formatter_of_buffer stdbuf]. *)
|
1999-02-16 01:07:26 -08:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val flush_str_formatter : unit -> string;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** Returns the material printed with [str_formatter], flushes
|
2002-05-08 06:50:29 -07:00
|
|
|
the formatter and resets the corresponding buffer. *)
|
1999-02-16 01:07:26 -08:00
|
|
|
|
2001-11-04 13:25:23 -08:00
|
|
|
val make_formatter :
|
2002-03-05 12:56:46 -08:00
|
|
|
(string -> int -> int -> unit) -> (unit -> unit) -> formatter;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [make_formatter out flush] returns a new formatter that
|
|
|
|
writes according to the output function [out], and the flushing
|
2001-11-04 13:25:23 -08:00
|
|
|
function [flush]. Hence, a formatter to the out channel [oc]
|
2001-10-26 15:37:14 -07:00
|
|
|
is returned by [make_formatter (output oc) (fun () -> flush oc)]. *)
|
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 Basic functions to use with formatters} *)
|
1996-07-08 11:53:26 -07:00
|
|
|
|
2002-03-05 12:56:46 -08:00
|
|
|
val pp_open_hbox : formatter -> unit -> unit;;
|
|
|
|
val pp_open_vbox : formatter -> int -> unit;;
|
|
|
|
val pp_open_hvbox : formatter -> int -> unit;;
|
|
|
|
val pp_open_hovbox : formatter -> int -> unit;;
|
|
|
|
val pp_open_box : formatter -> int -> unit;;
|
|
|
|
val pp_close_box : formatter -> unit -> unit;;
|
2002-03-11 14:18:20 -08:00
|
|
|
val pp_open_tag : formatter -> string -> unit;;
|
|
|
|
val pp_close_tag : formatter -> unit -> unit;;
|
2002-03-05 12:56:46 -08:00
|
|
|
val pp_print_string : formatter -> string -> unit;;
|
|
|
|
val pp_print_as : formatter -> int -> string -> unit;;
|
|
|
|
val pp_print_int : formatter -> int -> unit;;
|
|
|
|
val pp_print_float : formatter -> float -> unit;;
|
|
|
|
val pp_print_char : formatter -> char -> unit;;
|
|
|
|
val pp_print_bool : formatter -> bool -> unit;;
|
|
|
|
val pp_print_break : formatter -> int -> int -> unit;;
|
|
|
|
val pp_print_cut : formatter -> unit -> unit;;
|
|
|
|
val pp_print_space : formatter -> unit -> unit;;
|
|
|
|
val pp_force_newline : formatter -> unit -> unit;;
|
|
|
|
val pp_print_flush : formatter -> unit -> unit;;
|
|
|
|
val pp_print_newline : formatter -> unit -> unit;;
|
|
|
|
val pp_print_if_newline : formatter -> unit -> unit;;
|
|
|
|
val pp_open_tbox : formatter -> unit -> unit;;
|
|
|
|
val pp_close_tbox : formatter -> unit -> unit;;
|
|
|
|
val pp_print_tbreak : formatter -> int -> int -> unit;;
|
|
|
|
val pp_set_tab : formatter -> unit -> unit;;
|
|
|
|
val pp_print_tab : formatter -> unit -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
val pp_set_tags : formatter -> bool -> unit;;
|
2002-03-11 14:18:20 -08:00
|
|
|
val pp_set_print_tags : formatter -> bool -> unit;;
|
2002-03-21 08:23:40 -08:00
|
|
|
val pp_set_mark_tags : formatter -> bool -> unit;;
|
2002-03-22 12:43:07 -08:00
|
|
|
val pp_get_print_tags : formatter -> unit -> bool;;
|
|
|
|
val pp_get_mark_tags : formatter -> unit -> bool;;
|
2002-03-05 12:56:46 -08:00
|
|
|
val pp_set_margin : formatter -> int -> unit;;
|
|
|
|
val pp_get_margin : formatter -> unit -> int;;
|
|
|
|
val pp_set_max_indent : formatter -> int -> unit;;
|
|
|
|
val pp_get_max_indent : formatter -> unit -> int;;
|
|
|
|
val pp_set_max_boxes : formatter -> int -> unit;;
|
|
|
|
val pp_get_max_boxes : formatter -> unit -> int;;
|
|
|
|
val pp_over_max_boxes : formatter -> unit -> bool;;
|
|
|
|
val pp_set_ellipsis_text : formatter -> string -> unit;;
|
|
|
|
val pp_get_ellipsis_text : formatter -> unit -> string;;
|
|
|
|
val pp_set_formatter_out_channel : formatter -> out_channel -> unit;;
|
2001-12-03 14:01:28 -08:00
|
|
|
val pp_set_formatter_output_functions :
|
2002-03-05 12:56:46 -08:00
|
|
|
formatter -> (string -> int -> int -> unit) -> (unit -> unit) -> unit;;
|
2001-12-03 14:01:28 -08:00
|
|
|
val pp_get_formatter_output_functions :
|
2002-03-05 12:56:46 -08:00
|
|
|
formatter -> unit -> (string -> int -> int -> unit) * (unit -> unit);;
|
2001-12-03 14:01:28 -08:00
|
|
|
val pp_set_all_formatter_output_functions :
|
|
|
|
formatter -> out:(string -> int -> int -> unit) -> flush:(unit -> unit) ->
|
2002-03-05 12:56:46 -08:00
|
|
|
newline:(unit -> unit) -> spaces:(int -> unit) -> unit;;
|
2001-12-03 14:01:28 -08:00
|
|
|
val pp_get_all_formatter_output_functions :
|
|
|
|
formatter -> unit ->
|
2002-03-05 12:56:46 -08:00
|
|
|
(string -> int -> int -> unit) * (unit -> unit) * (unit -> unit) *
|
|
|
|
(int -> unit);;
|
2002-03-19 23:33:20 -08:00
|
|
|
val pp_set_formatter_tag_functions :
|
|
|
|
formatter -> formatter_tag_functions -> unit;;
|
|
|
|
val pp_get_formatter_tag_functions :
|
|
|
|
formatter -> unit -> formatter_tag_functions;;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** These functions are the basic ones: usual functions
|
|
|
|
operating on the standard formatter are defined via partial
|
|
|
|
evaluation of these primitives. For instance,
|
|
|
|
[print_string] is equal to [pp_print_string std_formatter]. *)
|
|
|
|
|
1997-09-05 11:26:53 -07:00
|
|
|
|
2001-12-28 15:13:35 -08:00
|
|
|
(** {6 [printf] like functions for pretty-printing.} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2003-07-05 04:13:24 -07:00
|
|
|
val fprintf : formatter -> ('a, formatter, unit) format -> 'a;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [fprintf ff format arg1 ... argN] formats the arguments
|
|
|
|
[arg1] to [argN] according to the format string [format],
|
|
|
|
and outputs the resulting string on the formatter [ff].
|
|
|
|
The format is a character string which contains three types of
|
|
|
|
objects: plain characters and conversion specifications as
|
|
|
|
specified in the [printf] module, and pretty-printing
|
|
|
|
indications.
|
|
|
|
The pretty-printing indication characters are introduced by
|
|
|
|
a [@] character, and their meanings are:
|
|
|
|
- [@\[]: open a pretty-printing box. The type and offset of the
|
|
|
|
box may be optionally specified with the following syntax:
|
|
|
|
the [<] character, followed by an optional box type indication,
|
|
|
|
then an optional integer offset, and the closing [>] character.
|
|
|
|
Box type is one of [h], [v], [hv], [b], or [hov],
|
|
|
|
which stand respectively for an horizontal box, a vertical box,
|
|
|
|
an ``horizontal-vertical'' box, or an ``horizontal or
|
|
|
|
vertical'' box ([b] standing for an ``horizontal or
|
|
|
|
vertical'' box demonstrating indentation and [hov] standing
|
|
|
|
for a regular``horizontal or vertical'' box).
|
|
|
|
For instance, [@\[<hov 2>] opens an ``horizontal or vertical''
|
|
|
|
box with indentation 2 as obtained with [open_hovbox 2].
|
|
|
|
For more details about boxes, see the various box opening
|
|
|
|
functions [open_*box].
|
|
|
|
- [@\]]: close the most recently opened pretty-printing box.
|
|
|
|
- [@,]: output a good break as with [print_cut ()].
|
|
|
|
- [@ ]: output a space, as with [print_space ()].
|
|
|
|
- [@\n]: force a newline, as with [force_newline ()].
|
|
|
|
- [@;]: output a good break as with [print_break]. The
|
|
|
|
[nspaces] and [offset] parameters of the break may be
|
|
|
|
optionally specified with the following syntax:
|
|
|
|
the [<] character, followed by an integer [nspaces] value,
|
|
|
|
then an integer offset, and a closing [>] character.
|
|
|
|
- [@?]: flush the pretty printer as with [print_flush ()].
|
2003-02-28 11:55:12 -08:00
|
|
|
This is equivalent to the conversion [%$].
|
2001-10-26 15:37:14 -07:00
|
|
|
- [@.]: flush the pretty printer and output a new line, as with
|
|
|
|
[print_newline ()].
|
|
|
|
- [@<n>]: print the following item as if it were of length [n].
|
|
|
|
Hence, [printf "@<0>%s" arg] is equivalent to [print_as 0 arg].
|
|
|
|
If [@<n>] is not followed by a conversion specification,
|
|
|
|
then the following character of the format is printed as if
|
|
|
|
it were of length [n].
|
2002-03-11 14:18:20 -08:00
|
|
|
- [@\{]: open a tag. The name of the tag may be optionally
|
|
|
|
specified with the following syntax:
|
|
|
|
the [<] character, followed by an optional string
|
|
|
|
specification, and the closing [>] character. The string
|
|
|
|
specification is any character string that does not contain the
|
|
|
|
closing character ['>']. If omitted, the tag name defaults to the
|
|
|
|
empty string.
|
|
|
|
For more details about tags, see the functions [open_tag] and
|
|
|
|
[close_tag].
|
|
|
|
- [@\}]: close the most recently opened tag.
|
2001-10-26 15:37:14 -07:00
|
|
|
- [@@]: print a plain [@] character.
|
2002-03-05 12:56:46 -08:00
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
Example: [printf "@[%s@ %d@]" "x =" 1] is equivalent to
|
|
|
|
[open_box (); print_string "x ="; print_space (); print_int 1; close_box ()].
|
2002-03-11 14:18:20 -08:00
|
|
|
It prints [x = 1] within a pretty-printing box.
|
|
|
|
*)
|
1997-09-05 11:26:53 -07:00
|
|
|
|
2003-07-05 04:13:24 -07:00
|
|
|
val printf : ('a, formatter, unit) format -> 'a;;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** Same as [fprintf] above, but output on [std_formatter]. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2003-07-05 04:13:24 -07:00
|
|
|
val eprintf : ('a, formatter, unit) format -> 'a;;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** Same as [fprintf] above, but output on [err_formatter]. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2003-07-05 04:13:24 -07:00
|
|
|
val sprintf : ('a, unit, string) format -> 'a;;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** Same as [printf] above, but instead of printing on a formatter,
|
2002-05-08 06:50:29 -07:00
|
|
|
returns a string containing the result of formatting the arguments.
|
2001-11-04 13:25:23 -08:00
|
|
|
Note that the pretty-printer queue is flushed at the end of each
|
|
|
|
call to [sprintf].
|
2002-03-05 12:56:46 -08:00
|
|
|
|
|
|
|
In case of multiple and related calls to [sprintf] to output
|
|
|
|
material on a single string, you should consider using [fprintf]
|
|
|
|
with a formatter writing to a buffer: flushing the buffer at the
|
|
|
|
end of pretty-printing returns the desired string. You can also use
|
|
|
|
the predefined formatter [str_formatter] and call
|
|
|
|
[flush_str_formatter ()] to get the result. *)
|
|
|
|
|
2003-07-05 04:13:24 -07:00
|
|
|
val bprintf : Buffer.t -> ('a, formatter, unit) format -> 'a;;
|
2001-11-04 13:25:23 -08:00
|
|
|
(** Same as [sprintf] above, but instead of printing on a string,
|
|
|
|
writes into the given extensible buffer.
|
|
|
|
As for [sprintf], the pretty-printer queue is flushed at the end of each
|
|
|
|
call to [bprintf].
|
2002-03-05 12:56:46 -08:00
|
|
|
|
|
|
|
In case of multiple and related calls to [bprintf] to output
|
|
|
|
material on the same buffer [b], you should consider using
|
|
|
|
[fprintf] with a formatter writing to the buffer [b] (as obtained
|
|
|
|
by [formatter_of_buffer b]), otherwise the repeated flushes of the
|
2002-05-08 06:50:29 -07:00
|
|
|
pretty-printer queue would result in unexpected and badly formatted
|
|
|
|
output. *)
|
2002-03-21 09:13:02 -08:00
|
|
|
|
2003-07-05 04:13:24 -07:00
|
|
|
val kprintf : (string -> 'a) -> ('b, unit, string, 'a) format4 -> 'b;;
|
2002-03-21 09:13:02 -08:00
|
|
|
(** Same as [sprintf] above, but instead of returning the string,
|
2002-05-08 06:50:29 -07:00
|
|
|
passes it to the first argument. *)
|