diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-15 14:47:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-12 13:30:57 +0100 |
| commit | 745eb8d6d9f99b69d11c16e8fb5e133e8e27d0a8 (patch) | |
| tree | 8e1a6a91449a2e8a7b15e6b5c04d3cbc61cdc3b5 /lib/pp.mli | |
| parent | 28fabbb1fbc35044fd257a2cad07fb70778c67fe (diff) | |
Improving spacing in printing disjunctive patterns.
Adding a space before the bar separating disjunctive patterns.
Removing an extra space after the bar for inner disjunctive patterns.
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 2d11cad86..d9be1c5ce 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -120,6 +120,9 @@ val pr_semicolon : unit -> t 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. *) |