Module Pp

Coq document type.

type pp_tag = string
type t
type block_type =
| Pp_hbox
| 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 : 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