Module `Pp`

Coq document type.

type pp_tag = string
type t
type block_type = | Pp_hbox of int | Pp_vbox of int | Pp_hvbox of int | Pp_hovbox of int
type doc_view = | Ppcmd_empty | Ppcmd_string of string | Ppcmd_glue of t list | Ppcmd_box of block_type * t | Ppcmd_tag of pp_tag * t | Ppcmd_print_break of int * int | Ppcmd_force_newline | Ppcmd_comment of string list

val repr : t -> doc_view
val unrepr : doc_view -> t

Formatting commands

val str : string -> t
val brk : (int * int) -> t
val fnl : unit -> t
val ws : int -> t
val mt : unit -> t
val ismt : t -> bool
val comment : string list -> t

Manipulation commands

val app : t -> t -> t: Concatenation.

val seq : t list -> t: Multi-Concatenation.

val (++) : t -> t -> t: Infix alias for app.

Derived commands

val spc : unit -> t
val cut : unit -> t
val align : unit -> t
val int : int -> t
val real : float -> t
val bool : bool -> t
val qstring : string -> t
val qs : string -> t
val quote : t -> t
val strbrk : string -> t

Boxing commands

val h : int -> t -> t
val v : int -> t -> t
val hv : int -> t -> t
val hov : int -> t -> t

Tagging

val tag : pp_tag -> t -> t

Printing combinators

val pr_comma : unit -> t: Well-spaced comma.

val pr_semicolon : unit -> t: Well-spaced semicolon.

val pr_bar : unit -> t: Well-spaced pipe bar.

val pr_spcbar : unit -> t: Pipe bar with space before and after.

val pr_arg : ('a -> t) -> 'a -> t: Adds a space in front of its argument.

val pr_non_empty_arg : ('a -> t) -> 'a -> t: Adds a space in front of its argument if non empty.

val pr_opt : ('a -> t) -> 'a option -> t: Inner object preceded with a space if Some, nothing otherwise.

val pr_opt_no_spc : ('a -> t) -> 'a option -> t: Same as pr_opt but without the leading space.

val pr_nth : int -> t: Ordinal number with the correct suffix (i.e. "st", "nd", "th", etc.).

val prlist : ('a -> t) -> 'a list -> t

Concatenation of the list contents, without any separator.

Unlike all other functions below, prlist works lazily. If a strict behavior is needed, use prlist_strict instead.

val prlist_strict : ('a -> t) -> 'a list -> t: Same as prlist, but strict.

val prlist_with_sep : (unit -> t) -> ('a -> t) -> 'a list -> t: prlist_with_sep sep pr [a ; ... ; c] outputs pr a ++ sep () ++ ... ++ sep () ++ pr c. where the thunk sep is memoized, rather than being called each place its result is used.

val prvect : ('a -> t) -> 'a array -> t: As prlist, but on arrays.

val prvecti : (int -> 'a -> t) -> 'a array -> t: Indexed version of prvect.

val prvect_with_sep : (unit -> t) -> ('a -> t) -> 'a array -> t: As prlist_with_sep, but on arrays.

val prvecti_with_sep : (unit -> t) -> (int -> 'a -> t) -> 'a array -> t: Indexed version of prvect_with_sep.

val pr_enum : ('a -> t) -> 'a list -> t: pr_enum pr [a ; b ; ... ; c] outputs pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c.

val pr_sequence : ('a -> t) -> 'a list -> t: Sequence of objects separated by space (unless an element is empty).

val surround : t -> t: Surround with parenthesis.

val pr_vertical_list : ('b -> t) -> 'b list -> t

Main renderers, to formatter and to string

val pp_with : Stdlib.Format.formatter -> t -> unit: pp_with fmt pp Print pp to fmt and don't flush fmt

val string_of_ppcmds : t -> string
val start_pfx : string: Tag prefix to start a multi-token diff span

val end_pfx : string: Tag prefix to end a multi-token diff span

val split_tag : string -> string * string: Split a tag into prefix and base tag

val db_print_pp : Stdlib.Format.formatter -> t -> unit: Print the Pp in tree form for debugging

val db_string_of_pp : t -> string: Print the Pp in tree form for debugging, return as a string

val flatten : t -> t: Combine nested Ppcmd_glues