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. --- printing/ppconstr.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 2abbc389f..2c03d7c8d 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -286,7 +286,7 @@ let tag_var = tag Tag.variable pr_reference r, latom | CPatOr pl -> - hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator + hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator | CPatNotation ("( _ )",([p],[]),[]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom @@ -315,7 +315,7 @@ let tag_var = tag Tag.variable spc() ++ hov 4 (pr_with_comments ?loc (str "| " ++ - hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl + hov 0 (prlist_with_sep pr_spcbar (prlist_with_sep sep_v (pr_patt ltop)) pl ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) -- cgit v1.2.3