diff options
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 6316ab410..614023758 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -16,9 +16,7 @@ val make_pp_nonemacs:unit -> unit (** Pretty-printers. *) -type ppcmd - -type std_ppcmds = ppcmd Stream.t +type std_ppcmds (** {6 Formatting commands} *) @@ -36,13 +34,19 @@ val ismt : std_ppcmds -> bool val comment : int -> std_ppcmds val comments : ((int * int) * string) list ref -(** {6 Concatenation. } *) +(** {6 Manipulation commands} *) -val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds +val app : std_ppcmds -> std_ppcmds -> std_ppcmds +(** Concatenation. *) -(** {6 Evaluation} *) +val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds +(** Infix alias for [app]. *) val eval_ppcmds : std_ppcmds -> std_ppcmds +(** Force computation. *) + +val is_empty : std_ppcmds -> bool +(** Test emptyness. *) (** {6 Derived commands} *) @@ -57,7 +61,7 @@ val qs : string -> std_ppcmds val quote : std_ppcmds -> std_ppcmds val strbrk : string -> std_ppcmds -val xmlescape : ppcmd -> ppcmd +val xmlescape : std_ppcmds -> std_ppcmds (** {6 Boxing commands} *) |