summaryrefslogtreecommitdiff
path: root/lib/pp.mli
diff options
context:
space:
mode:
Diffstat (limited to 'lib/pp.mli')
-rw-r--r--lib/pp.mli19
1 files changed, 19 insertions, 0 deletions
diff --git a/lib/pp.mli b/lib/pp.mli
index f3a0a29b..ed31daa5 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -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