aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-15 14:47:15 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-12-12 13:30:57 +0100
commit745eb8d6d9f99b69d11c16e8fb5e133e8e27d0a8 (patch)
tree8e1a6a91449a2e8a7b15e6b5c04d3cbc61cdc3b5 /lib
parent28fabbb1fbc35044fd257a2cad07fb70778c67fe (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')
-rw-r--r--lib/pp.ml1
-rw-r--r--lib/pp.mli3
2 files changed, 4 insertions, 0 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index c3338688d..770e650cb 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -208,6 +208,7 @@ let string_of_ppcmds c =
let pr_comma () = str "," ++ spc ()
let pr_semicolon () = str ";" ++ spc ()
let pr_bar () = str "|" ++ spc ()
+let pr_spcbar () = 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
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. *)