diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /lib/pp.mli | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'lib/pp.mli')
-rw-r--r-- | lib/pp.mli | 19 |
1 files changed, 19 insertions, 0 deletions
@@ -189,3 +189,22 @@ val pr_vertical_list : ('b -> t) -> 'b list -> t val pp_with : Format.formatter -> t -> unit val string_of_ppcmds : t -> string + + +(** Tag prefix to start a multi-token diff span *) +val start_pfx : string + +(** Tag prefix to end a multi-token diff span *) +val end_pfx : string + +(** Split a tag into prefix and base tag *) +val split_tag : string -> string * string + +(** Print the Pp in tree form for debugging *) +val db_print_pp : Format.formatter -> t -> unit + +(** Print the Pp in tree form for debugging, return as a string *) +val db_string_of_pp : t -> string + +(** Combine nested Ppcmd_glues *) +val flatten : t -> t |