aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
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 /printing/ppconstr.ml
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 'printing/ppconstr.ml')
-rw-r--r--printing/ppconstr.ml4
1 files changed, 2 insertions, 2 deletions
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))