1995-08-09 08:06:35 -07:00
|
|
|
(***********************************************************************)
|
|
|
|
(* *)
|
2011-07-27 07:17:02 -07:00
|
|
|
(* OCaml *)
|
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
|
|
|
(* *)
|
|
|
|
(***********************************************************************)
|
|
|
|
|
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
|
2013-05-29 11:03:55 -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.
|
|
|
|
|
2005-07-22 05:22:29 -07:00
|
|
|
For a gentle introduction to the basics of pretty-printing using
|
2005-08-13 13:59:37 -07:00
|
|
|
[Format], read
|
2012-03-08 14:36:21 -08:00
|
|
|
{{:http://caml.inria.fr/resources/doc/guides/format.en.html}
|
|
|
|
http://caml.inria.fr/resources/doc/guides/format.en.html}.
|
2004-06-04 01:01:31 -07:00
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
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
|
|
|
|
2005-08-13 13:59:37 -07:00
|
|
|
For instance, the sequence
|
2009-11-30 14:04:17 -08:00
|
|
|
[open_box 0; print_string "x ="; print_space ();
|
|
|
|
print_int 1; close_box (); print_newline ()]
|
1998-12-08 00:29:54 -08:00
|
|
|
that prints [x = 1] within a pretty-printing box, can be
|
2009-11-30 14:04:17 -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;
|
2009-11-30 14:04:17 -08:00
|
|
|
- at the end of your routine, flush the pretty-printer to display all the
|
|
|
|
remaining material, e.g. evaluate [print_newline ()].
|
2001-10-26 15:37:14 -07:00
|
|
|
|
|
|
|
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.
|
2006-11-17 00:37:07 -08:00
|
|
|
|
|
|
|
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
|
|
|
|
the evaluation order of printing commands.
|
2001-10-26 15:37:14 -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.
|
2013-05-29 11:03:55 -07:00
|
|
|
Material in this box is displayed 'horizontal or vertical':
|
2001-10-26 15:37:14 -07:00
|
|
|
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-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
|
2005-07-22 05:22:29 -07:00
|
|
|
a space between two words).
|
2001-10-26 15:37:14 -07:00
|
|
|
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.
|
2005-07-22 05:22:29 -07:00
|
|
|
It indicates that the line may be split at this
|
2001-10-26 15:37:14 -07:00
|
|
|
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
|
2005-07-22 05:22:29 -07:00
|
|
|
current line.
|
2001-10-26 15:37:14 -07:00
|
|
|
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-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.
|
2004-07-13 05:25:21 -07:00
|
|
|
Nothing happens if [d] is smaller than 2.
|
|
|
|
If [d] is too large, the right margin is set to the maximum
|
2012-10-05 08:21:35 -07:00
|
|
|
admissible value (which is greater than [10^9]). *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
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-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.
|
2004-07-13 05:25:21 -07:00
|
|
|
Nothing happens if [d] is smaller than 2.
|
|
|
|
If [d] is too large, the limit is set to the maximum
|
2012-10-05 08:21:35 -07:00
|
|
|
admissible value (which is greater than [10^9]). *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
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-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;;
|
2013-03-19 12:25:24 -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 [get_ellipsis_text ()]).
|
2004-07-13 05:25:21 -07:00
|
|
|
Nothing happens if [max] is smaller than 2. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
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-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.
|
2013-05-29 11:03:55 -07:00
|
|
|
This box is 'horizontal': the line is not split in this box
|
2001-10-26 15:37:14 -07:00
|
|
|
(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].
|
2013-05-29 11:03:55 -07:00
|
|
|
This box is 'vertical': every break hint inside this
|
2001-10-26 15:37:14 -07:00
|
|
|
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].
|
2013-05-29 11:03:55 -07:00
|
|
|
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.
|
2001-10-26 15:37:14 -07:00
|
|
|
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].
|
2013-05-29 11:03:55 -07:00
|
|
|
This box is 'horizontal or vertical': break hints
|
2001-10-26 15:37:14 -07:00
|
|
|
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;;
|
2009-04-01 09:34:55 -07:00
|
|
|
(** [print_tab ()] is equivalent to [print_tbreak 0 0]. *)
|
1997-05-13 11:27:27 -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. *)
|
|
|
|
|
2010-01-22 08:57:26 -08:00
|
|
|
(** {6:tags Semantics Tags} *)
|
2002-03-11 14:18:20 -08:00
|
|
|
|
2002-05-08 06:50:29 -07:00
|
|
|
type tag = string;;
|
2002-03-11 14:18:20 -08:00
|
|
|
|
2009-11-30 14:04:17 -08:00
|
|
|
(** {i Semantics tags} (or simply {e tags}) are used to decorate printed
|
|
|
|
entities for user's defined purposes, e.g. setting font and giving size
|
|
|
|
indications for a display device, or marking delimitation of semantics
|
|
|
|
entities (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:
|
2013-05-29 11:03:55 -07:00
|
|
|
the tag 'markers' are not considered as part of the printing
|
2003-09-25 03:33:52 -07:00
|
|
|
material that drives line breaking (in other words, the length of
|
2002-05-08 06:50:29 -07:00
|
|
|
those strings is considered as zero for line breaking).
|
|
|
|
|
|
|
|
Thus, tag handling is in some sense transparent to pretty-printing
|
2012-04-27 02:56:05 -07:00
|
|
|
and does not interfere with usual indentation. Hence, a single
|
2013-05-29 11:03:55 -07:00
|
|
|
pretty printing routine can output both simple 'verbatim'
|
2002-05-08 06:50:29 -07:00
|
|
|
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
|
2010-01-22 08:57:26 -08:00
|
|
|
decorated with tag information. Once [set_tags] is set to [true],
|
2009-11-30 14:04:17 -08:00
|
|
|
the pretty printer engine honours tags and decorates the output
|
2003-09-25 00:43:54 -07:00
|
|
|
accordingly.
|
2002-05-08 06:50:29 -07:00
|
|
|
|
|
|
|
When a tag has been opened (or closed), it is both and successively
|
2013-05-29 11:03:55 -07:00
|
|
|
'printed' and 'marked'. Printing a tag means calling a
|
2002-05-08 06:50:29 -07:00
|
|
|
formatter specific function with the name of the tag as argument:
|
2013-05-29 11:03:55 -07:00
|
|
|
that 'tag printing' function can then print any regular material
|
2002-05-08 06:50:29 -07:00
|
|
|
to the formatter (so that this material is enqueued as usual in the
|
|
|
|
formatter queue for further line-breaking computation). Marking a
|
2013-05-29 11:03:55 -07:00
|
|
|
tag means to output an arbitrary string (the 'tag marker'),
|
2002-05-08 06:50:29 -07:00
|
|
|
directly into the output device of the formatter. Hence, the
|
2013-05-29 11:03:55 -07:00
|
|
|
formatter specific 'tag marking' function must return the tag
|
2002-05-08 06:50:29 -07:00
|
|
|
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
|
2003-09-25 03:33:52 -07:00
|
|
|
drives line breaking (in other words, the length of the strings
|
2002-05-08 06:50:29 -07:00
|
|
|
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. *)
|
2013-03-19 12:25:24 -07:00
|
|
|
|
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;;
|
2003-09-25 03:33:52 -07:00
|
|
|
(** Return the current status of tags printing and tags marking. *)
|
2002-03-11 14:18:20 -08:00
|
|
|
|
2009-11-30 14:04:17 -08:00
|
|
|
(** {6 Redirecting the standard formatter output} *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2009-07-03 03:46:10 -07:00
|
|
|
val set_formatter_out_channel : Pervasives.out_channel -> unit;;
|
2010-05-03 00:09:33 -07:00
|
|
|
(** Redirect the pretty-printer output to the given channel.
|
|
|
|
(All the output functions of the standard formatter are set to the
|
|
|
|
default output functions printing 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 :
|
2010-05-03 02:17:37 -07:00
|
|
|
(string -> int -> int -> unit) -> (unit -> unit) -> unit
|
|
|
|
;;
|
2001-10-26 15:37:14 -07:00
|
|
|
(** [set_formatter_output_functions out flush] redirects the
|
2013-03-19 12:25:24 -07:00
|
|
|
pretty-printer output functions to the functions [out] and
|
2010-05-03 00:09:33 -07:00
|
|
|
[flush].
|
2002-03-05 12:56:46 -08:00
|
|
|
|
2013-03-19 12:25:24 -07:00
|
|
|
The [out] function performs all the pretty-printer string 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
|
|
|
|
(via conversion [%!], or pretty-printing indications [@?] or [@.], or
|
|
|
|
using low level functions [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 :
|
2010-05-03 02:17:37 -07: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
|
|
|
|
2010-04-15 01:39:16 -07:00
|
|
|
(** {6:meaning Changing the meaning of standard formatter pretty printing} *)
|
2010-01-20 08:26:46 -08:00
|
|
|
|
2012-04-27 05:13:29 -07:00
|
|
|
(** The [Format] module is versatile enough to let you completely redefine
|
|
|
|
the meaning of pretty printing: you may provide your own functions to define
|
|
|
|
how to handle indentation, line breaking, and even printing of all the
|
|
|
|
characters that have to be printed! *)
|
|
|
|
|
2012-04-27 02:56:05 -07:00
|
|
|
type formatter_out_functions = {
|
|
|
|
out_string : string -> int -> int -> unit;
|
|
|
|
out_flush : unit -> unit;
|
|
|
|
out_newline : unit -> unit;
|
|
|
|
out_spaces : int -> unit;
|
|
|
|
}
|
|
|
|
;;
|
|
|
|
|
2013-03-19 00:58:59 -07:00
|
|
|
val set_formatter_out_functions : formatter_out_functions -> unit;;
|
2014-01-22 06:05:13 -08:00
|
|
|
(** [set_formatter_out_functions f]
|
|
|
|
Redirect the pretty-printer output to the functions [f.out_string]
|
|
|
|
and [f.out_flush] as described in
|
2013-03-19 12:25:24 -07:00
|
|
|
[set_formatter_output_functions]. In addition, the pretty-printer function
|
2014-01-22 06:05:13 -08:00
|
|
|
that outputs a newline is set to the function [f.out_newline] and
|
2013-03-19 12:25:24 -07:00
|
|
|
the function that outputs indentation spaces is set to the function
|
2014-01-22 06:05:13 -08:00
|
|
|
[f.out_spaces].
|
2012-04-27 02:56:05 -07:00
|
|
|
|
2012-04-27 05:13:29 -07:00
|
|
|
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
|
2014-01-22 06:05:13 -08:00
|
|
|
application at hand). The two functions [f.out_spaces] and [f.out_newline]
|
|
|
|
are normally connected to [f.out_string] and [f.out_flush]: respective
|
|
|
|
default values for [f.out_space] and [f.out_newline] are
|
|
|
|
[f.out_string (String.make n ' ') 0 n] and [f.out_string "\n" 0 1]. *)
|
2012-04-27 05:13:29 -07:00
|
|
|
|
2013-03-19 00:58:59 -07:00
|
|
|
val get_formatter_out_functions : unit -> formatter_out_functions;;
|
2012-04-27 05:13:29 -07:00
|
|
|
(** Return the current output functions of the pretty-printer,
|
|
|
|
including line breaking and indentation functions. Useful to record the
|
|
|
|
current setting and restore it afterwards. *)
|
2010-01-20 08:26:46 -08:00
|
|
|
|
2012-02-21 04:41:33 -08:00
|
|
|
(** {6:tagsmeaning Changing the meaning of printing semantics 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;
|
2010-05-03 02:17:37 -07:00
|
|
|
}
|
|
|
|
;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** The tag handling functions specific to a formatter:
|
2013-05-29 11:03:55 -07:00
|
|
|
[mark] versions are the 'tag marking' functions that associate a string
|
2002-05-08 06:50:29 -07:00
|
|
|
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.
|
2013-05-29 11:03:55 -07:00
|
|
|
[print] versions are the 'tag printing' functions that can perform
|
2002-05-08 06:50:29 -07:00
|
|
|
regular printing when a tag is closed or opened. *)
|
|
|
|
|
2012-04-27 05:13:29 -07:00
|
|
|
val set_formatter_tag_functions : formatter_tag_functions -> unit;;
|
2002-05-08 06:50:29 -07:00
|
|
|
(** [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
|
|
|
|
2012-04-27 05:13:29 -07:00
|
|
|
val get_formatter_tag_functions : unit -> formatter_tag_functions;;
|
2010-04-15 01:39:16 -07:00
|
|
|
(** Return the current tag functions of the pretty-printer. *)
|
2009-01-25 14:46:15 -08:00
|
|
|
|
2010-01-22 08:57:26 -08:00
|
|
|
(** {6 Multiple formatted output} *)
|
|
|
|
|
2010-04-15 01:39:16 -07:00
|
|
|
type formatter;;
|
|
|
|
(** Abstract data corresponding to a pretty-printer (also called a
|
2010-05-03 02:17:37 -07:00
|
|
|
formatter) and all its machinery.
|
|
|
|
|
|
|
|
Defining new pretty-printers permits unrelated output of material in
|
|
|
|
parallel on several output channels.
|
|
|
|
All the parameters of a pretty-printer are local to this pretty-printer:
|
2010-04-15 01:39:16 -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.
|
2010-05-03 02:17:37 -07:00
|
|
|
Given a [Pervasives.out_channel] output channel [oc], a new formatter
|
|
|
|
writing to that channel is simply obtained by calling
|
|
|
|
[formatter_of_out_channel oc].
|
2010-04-15 01:39:16 -07:00
|
|
|
Alternatively, the [make_formatter] function allocates a new
|
|
|
|
formatter with explicit output and flushing functions
|
2010-05-03 02:17:37 -07:00
|
|
|
(convenient to output material to strings for instance).
|
|
|
|
*)
|
2010-04-15 01:39:16 -07: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
|
2010-04-15 01:39:16 -07:00
|
|
|
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;;
|
2010-04-15 01:39:16 -07:00
|
|
|
(** The standard formatter used by the formatting functions
|
|
|
|
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;;
|
2010-04-15 01:39:16 -07:00
|
|
|
(** A formatter to use with formatting functions below for
|
|
|
|
output to standard error. It is defined as
|
|
|
|
[formatter_of_out_channel stderr]. *)
|
|
|
|
|
|
|
|
val formatter_of_buffer : Buffer.t -> formatter;;
|
|
|
|
(** [formatter_of_buffer b] returns a new formatter writing to
|
|
|
|
buffer [b]. As usual, the formatter has to be flushed at
|
|
|
|
the end of pretty printing, using [pp_print_flush] or
|
|
|
|
[pp_print_newline], to display all the pending material. *)
|
|
|
|
|
|
|
|
val stdbuf : Buffer.t;;
|
|
|
|
(** 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;;
|
2010-04-15 01:39:16 -07:00
|
|
|
(** A formatter to use with formatting functions below for
|
|
|
|
output to the [stdbuf] string buffer.
|
|
|
|
[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;;
|
2010-04-15 01:39:16 -07:00
|
|
|
(** Returns the material printed with [str_formatter], flushes
|
|
|
|
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 :
|
2010-05-03 02:17:37 -07:00
|
|
|
(string -> int -> int -> unit) -> (unit -> unit) -> formatter
|
|
|
|
;;
|
|
|
|
(** [make_formatter out flush] returns a new formatter that writes according
|
|
|
|
to the output function [out], and the flushing function [flush]. For
|
|
|
|
instance, a formatter to the [Pervasives.out_channel] [oc] is returned by
|
|
|
|
[make_formatter (Pervasives.output oc) (fun () -> Pervasives.flush oc)]. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
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;;
|
2013-03-19 12:25:24 -07:00
|
|
|
val pp_set_formatter_out_channel :
|
|
|
|
formatter -> Pervasives.out_channel -> unit
|
|
|
|
;;
|
2001-12-03 14:01:28 -08:00
|
|
|
val pp_set_formatter_output_functions :
|
2010-05-03 02:17:37 -07:00
|
|
|
formatter -> (string -> int -> int -> unit) -> (unit -> unit) -> unit
|
|
|
|
;;
|
2001-12-03 14:01:28 -08:00
|
|
|
val pp_get_formatter_output_functions :
|
2010-05-03 02:17:37 -07:00
|
|
|
formatter -> unit -> (string -> int -> int -> unit) * (unit -> unit)
|
|
|
|
;;
|
2002-03-19 23:33:20 -08:00
|
|
|
val pp_set_formatter_tag_functions :
|
2010-05-03 02:17:37 -07:00
|
|
|
formatter -> formatter_tag_functions -> unit
|
|
|
|
;;
|
2002-03-19 23:33:20 -08:00
|
|
|
val pp_get_formatter_tag_functions :
|
2010-05-03 02:17:37 -07:00
|
|
|
formatter -> unit -> formatter_tag_functions
|
|
|
|
;;
|
2013-03-19 00:58:59 -07:00
|
|
|
val pp_set_formatter_out_functions :
|
|
|
|
formatter -> formatter_out_functions -> unit
|
|
|
|
;;
|
2013-03-19 03:14:31 -07:00
|
|
|
val pp_get_formatter_out_functions :
|
2013-03-19 00:58:59 -07:00
|
|
|
formatter -> unit -> formatter_out_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,
|
2010-04-15 01:39:16 -07:00
|
|
|
[print_string] is equal to [pp_print_string std_formatter]. *)
|
2001-11-04 13:25:23 -08:00
|
|
|
|
2013-09-13 08:55:41 -07:00
|
|
|
(** {6 Convenience formatting functions.} *)
|
|
|
|
|
|
|
|
val pp_print_list:
|
2014-01-22 06:05:13 -08:00
|
|
|
?pp_sep:(formatter -> unit -> unit) ->
|
2013-09-13 08:55:41 -07:00
|
|
|
(formatter -> 'a -> unit) -> (formatter -> 'a list -> unit)
|
|
|
|
(** [pp_print_list ?pp_sep pp_v ppf l] prints the list [l]. [pp_v] is
|
|
|
|
used on the elements of [l] and each element is separated by
|
|
|
|
a call to [pp_sep] (defaults to {!pp_print_cut}). Does nothing on
|
|
|
|
empty lists.
|
|
|
|
|
2014-01-22 06:05:13 -08:00
|
|
|
@since 4.02.0
|
2013-09-13 08:55:41 -07:00
|
|
|
*)
|
|
|
|
|
|
|
|
val pp_print_text : formatter -> string -> unit
|
|
|
|
(** [pp_print_text ppf s] prints [s] with spaces and newlines
|
|
|
|
respectively printed with {!pp_print_space} and
|
|
|
|
{!pp_force_newline}.
|
|
|
|
|
2014-01-22 06:05:13 -08:00
|
|
|
@since 4.02.0
|
2013-09-13 08:55:41 -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
|
|
|
|
2010-04-15 01:39:16 -07:00
|
|
|
val fprintf : formatter -> ('a, formatter, unit) format -> 'a;;
|
2010-05-03 02:17:37 -07:00
|
|
|
|
|
|
|
(** [fprintf ff fmt arg1 ... argN] formats the arguments [arg1] to [argN]
|
|
|
|
according to the format string [fmt], and outputs the resulting string on
|
|
|
|
the formatter [ff].
|
|
|
|
|
|
|
|
The format [fmt] 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 specific to the
|
|
|
|
[Format] module.
|
|
|
|
|
2001-10-26 15:37:14 -07:00
|
|
|
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,
|
2005-08-13 13:59:37 -07:00
|
|
|
then an optional integer offset, and the closing [>] character.
|
2001-10-26 15:37:14 -07:00
|
|
|
Box type is one of [h], [v], [hv], [b], or [hov],
|
|
|
|
which stand respectively for an horizontal box, a vertical box,
|
2013-05-29 11:03:55 -07:00
|
|
|
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'
|
2001-10-26 15:37:14 -07:00
|
|
|
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.
|
2013-03-19 00:58:59 -07:00
|
|
|
- [@,]: output a good break hint, as with [print_cut ()].
|
|
|
|
- [@ ]: output a good break space, as with [print_space ()].
|
|
|
|
- [@;]: output a fully specified good break as with [print_break]. The
|
2001-10-26 15:37:14 -07:00
|
|
|
[nspaces] and [offset] parameters of the break may be
|
2005-08-13 13:59:37 -07:00
|
|
|
optionally specified with the following syntax:
|
2001-10-26 15:37:14 -07:00
|
|
|
the [<] character, followed by an integer [nspaces] value,
|
2006-10-04 02:42:45 -07:00
|
|
|
then an integer [offset], and a closing [>] character.
|
2004-06-04 01:01:31 -07:00
|
|
|
If no parameters are provided, the good break defaults to a
|
2013-03-19 00:58:59 -07:00
|
|
|
good break space.
|
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].
|
2011-10-25 06:13:54 -07:00
|
|
|
Hence, [printf "@<0>%s" arg] prints [arg] as a zero length string.
|
2001-10-26 15:37:14 -07:00
|
|
|
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.
|
2013-03-19 00:58:59 -07:00
|
|
|
- [@?]: flush the pretty printer as with [print_flush ()].
|
|
|
|
This is equivalent to the conversion [%!].
|
|
|
|
- [@\n]: force a newline, as with [force_newline ()].
|
2013-05-29 08:56:25 -07:00
|
|
|
- [@@]: print a single [@] character.
|
2002-03-05 12:56:46 -08:00
|
|
|
|
2009-11-30 14:04:17 -08:00
|
|
|
Example: [printf "@[%s@ %d@]@." "x =" 1] is equivalent to
|
|
|
|
[open_box (); print_string "x ="; print_space ();
|
|
|
|
print_int 1; close_box (); print_newline ()].
|
2002-03-11 14:18:20 -08:00
|
|
|
It prints [x = 1] within a pretty-printing box.
|
2012-03-08 11:52:03 -08:00
|
|
|
|
2013-03-19 03:14:31 -07:00
|
|
|
Note: If you need to prevent the interpretation of a [@] character as a
|
2014-01-22 06:05:13 -08:00
|
|
|
pretty-printing indication, you can also escape it with a [%] character.
|
2012-03-08 11:52:03 -08:00
|
|
|
|
2002-03-11 14:18:20 -08:00
|
|
|
*)
|
1997-09-05 11:26:53 -07:00
|
|
|
|
2010-04-15 01:39:16 -07:00
|
|
|
val printf : ('a, formatter, unit) format -> 'a;;
|
|
|
|
(** Same as [fprintf] above, but output on [std_formatter]. *)
|
2009-09-09 08:15:03 -07:00
|
|
|
|
2010-04-15 01:39:16 -07:00
|
|
|
val eprintf : ('a, formatter, unit) format -> 'a;;
|
|
|
|
(** Same as [fprintf] above, but output on [err_formatter]. *)
|
2001-10-26 15:37:14 -07:00
|
|
|
|
2013-04-25 02:14:09 -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.
|
2009-11-30 14:04:17 -08:00
|
|
|
Note that the pretty-printer queue is flushed at the end of {e 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]
|
2010-05-03 02:17:37 -07:00
|
|
|
with the predefined formatter [str_formatter] and call
|
|
|
|
[flush_str_formatter ()] to get the final result.
|
2010-04-15 01:39:16 -07:00
|
|
|
|
2010-05-03 02:17:37 -07:00
|
|
|
Alternatively, you can use [Format.fprintf] with a formatter writing to a
|
|
|
|
buffer of your own: flushing the formatter and the buffer at the end of
|
2013-03-19 00:58:59 -07:00
|
|
|
pretty-printing returns the desired string.
|
2013-04-25 02:14:09 -07:00
|
|
|
*)
|
2013-03-19 00:58:59 -07:00
|
|
|
|
2013-04-25 02:14:09 -07:00
|
|
|
val asprintf : ('a, formatter, unit, string) format4 -> 'a;;
|
|
|
|
(** Same as [printf] above, but instead of printing on a formatter,
|
|
|
|
returns a string containing the result of formatting the arguments.
|
|
|
|
The type of [asprintf] is general enough to interact nicely with [%a]
|
2013-03-19 12:25:24 -07:00
|
|
|
conversions.
|
|
|
|
@since 4.01.0
|
2013-03-19 00:58:59 -07:00
|
|
|
*)
|
2010-05-03 02:17:37 -07:00
|
|
|
|
|
|
|
val ifprintf : formatter -> ('a, formatter, unit) format -> 'a;;
|
|
|
|
(** Same as [fprintf] above, but does not print anything.
|
2010-05-21 11:30:12 -07:00
|
|
|
Useful to ignore some material when conditionally printing.
|
|
|
|
@since 3.10.0
|
|
|
|
*)
|
2009-07-03 03:32:45 -07:00
|
|
|
|
|
|
|
(** Formatted output functions with continuations. *)
|
|
|
|
|
2010-04-15 01:39:16 -07:00
|
|
|
val kfprintf : (formatter -> 'a) -> formatter ->
|
2010-05-03 02:17:37 -07:00
|
|
|
('b, formatter, unit, 'a) format4 -> 'b
|
|
|
|
;;
|
2003-10-27 00:59:08 -08:00
|
|
|
(** Same as [fprintf] above, but instead of returning immediately,
|
|
|
|
passes the formatter to its first argument at the end of printing. *)
|
|
|
|
|
2010-04-15 01:39:16 -07:00
|
|
|
val ikfprintf : (formatter -> 'a) -> formatter ->
|
2010-05-03 02:17:37 -07:00
|
|
|
('b, formatter, unit, 'a) format4 -> 'b
|
|
|
|
;;
|
2009-09-09 08:15:03 -07:00
|
|
|
(** Same as [kfprintf] above, but does not print anything.
|
2010-05-21 11:30:12 -07:00
|
|
|
Useful to ignore some material when conditionally printing.
|
|
|
|
@since 3.12.0
|
|
|
|
*)
|
2009-09-09 08:15:03 -07:00
|
|
|
|
2003-10-27 00:59:08 -08:00
|
|
|
val ksprintf : (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. *)
|
2003-10-27 00:59:08 -08:00
|
|
|
|
2010-05-03 02:17:37 -07:00
|
|
|
(** {6 Deprecated} *)
|
|
|
|
|
|
|
|
val bprintf : Buffer.t -> ('a, formatter, unit) format -> 'a;;
|
2014-01-22 06:05:13 -08:00
|
|
|
(** @deprecated This function is error prone. Do not use it.
|
2010-05-03 02:17:37 -07:00
|
|
|
|
|
|
|
If you need to print to some buffer [b], you must first define a
|
|
|
|
formatter writing to [b], using [let to_b = formatter_of_buffer b]; then
|
|
|
|
use regular calls to [Format.fprintf] on formatter [to_b]. *)
|
|
|
|
|
2003-10-27 00:59:08 -08:00
|
|
|
val kprintf : (string -> 'a) -> ('b, unit, string, 'a) format4 -> 'b;;
|
2014-01-22 06:05:13 -08:00
|
|
|
(** @deprecated An alias for [ksprintf]. *)
|
2013-03-19 00:58:59 -07:00
|
|
|
|
|
|
|
val set_all_formatter_output_functions :
|
|
|
|
out:(string -> int -> int -> unit) ->
|
|
|
|
flush:(unit -> unit) ->
|
|
|
|
newline:(unit -> unit) ->
|
|
|
|
spaces:(int -> unit) ->
|
|
|
|
unit
|
|
|
|
;;
|
2014-01-22 06:05:13 -08:00
|
|
|
(** @deprecated Subsumed by [set_formatter_out_functions].
|
2013-03-19 00:58:59 -07:00
|
|
|
*)
|
|
|
|
|
|
|
|
val get_all_formatter_output_functions :
|
|
|
|
unit ->
|
|
|
|
(string -> int -> int -> unit) *
|
|
|
|
(unit -> unit) *
|
|
|
|
(unit -> unit) *
|
|
|
|
(int -> unit)
|
|
|
|
;;
|
2014-01-22 06:05:13 -08:00
|
|
|
(** @deprecated Subsumed by [get_formatter_out_functions].
|
2013-03-19 00:58:59 -07:00
|
|
|
*)
|
|
|
|
val pp_set_all_formatter_output_functions :
|
|
|
|
formatter -> out:(string -> int -> int -> unit) -> flush:(unit -> unit) ->
|
|
|
|
newline:(unit -> unit) -> spaces:(int -> unit) -> unit
|
|
|
|
;;
|
2014-01-22 06:05:13 -08:00
|
|
|
(** @deprecated Subsumed by [pp_set_formatter_out_functions].
|
2013-03-19 00:58:59 -07:00
|
|
|
*)
|
|
|
|
|
|
|
|
val pp_get_all_formatter_output_functions :
|
|
|
|
formatter -> unit ->
|
|
|
|
(string -> int -> int -> unit) * (unit -> unit) * (unit -> unit) *
|
|
|
|
(int -> unit)
|
|
|
|
;;
|
2014-01-22 06:05:13 -08:00
|
|
|
(** @deprecated Subsumed by [pp_get_formatter_out_functions].
|
2013-03-19 00:58:59 -07:00
|
|
|
*)
|