diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/pp.ml | 1 | ||||
| -rw-r--r-- | lib/pp.mli | 3 |
2 files changed, 4 insertions, 0 deletions
@@ -518,6 +518,7 @@ let pr_comma () = str "," ++ spc () let pr_semicolon () = str ";" ++ spc () let pr_bar () = str "|" ++ spc () let pr_arg pr x = spc () ++ pr x +let pr_non_empty_arg pr x = let pp = pr x in if ismt pp then mt () else spc () ++ pr x let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x diff --git a/lib/pp.mli b/lib/pp.mli index 015151bc90..2e4d029749 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -199,6 +199,9 @@ val pr_bar : unit -> std_ppcmds val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds (** Adds a space in front of its argument. *) +val pr_non_empty_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds +(** Adds a space in front of its argument if non empty. *) + val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds (** Inner object preceded with a space if [Some], nothing otherwise. *) |