From 745eb8d6d9f99b69d11c16e8fb5e133e8e27d0a8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 14:47:15 +0200 Subject: 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. --- lib/pp.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'lib/pp.ml') 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 -- cgit v1.2.3