Protect printing of intro-patterns from collision when "[|" or "|]"

exist as a keyword by inserting a space inbetween.

1 files changed, 10 insertions, 3 deletions

diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 7b2c5695f..1fbf703f5 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -36,9 +36,16 @@ and pr_or_and_intro_pattern prc = function
   | IntroAndPattern pl ->
       str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")"
   | IntroOrPattern pll ->
-      str "[" ++
-      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
-      ++ str "]"
+      let n = List.length pll in
+      let pll = Util.List.map_i (fun i l ->
+        if Util.List.is_empty l then
+          if i=1 then if Lexer.is_keyword "[|" then spc () else mt () else
+          if i=n then if Lexer.is_keyword "|]" then spc () else mt () else
+            spc () (* because || is a keyword *)
+        else
+          prlist_with_sep spc (pr_intro_pattern prc) l) 1 pll in
+      str "[" ++ hv 0 (prlist_with_sep (fun () -> str "|") (fun x -> x) pll) ++
+      str "]"
 
 (** Printing of [move_location] *)