diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-12-14 17:22:07 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-14 17:22:07 +0100 |
commit | 84e570d7c532f16104157b806da714906fdf26b3 (patch) | |
tree | f020dcc0e2e599ae02d045240a076900595ea056 /lib | |
parent | 8f936f45ab95fdb72f1d596fc621faa39ddcb95e (diff) | |
parent | 7720a01ceb7d00bc16cd96d99c27bc7696388899 (diff) |
Merge PR #978: In printing, experimenting factorizing "match" clauses with same right-hand side.
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
@@ -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. *) |