diff options
| author | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
| commit | 3a95d20e88474ecf95f66ba0ac1ff7729be496c7 (patch) | |
| tree | 50d76b54bf2e3a21e09226a7121272745bbb56dc | |
| parent | 74223731f771f01f71aad219056abc7dd9133631 (diff) | |
Revert "Protect printing of intro-patterns from collision when "[|" or "|]""
This reverts commit e9abd74adc486c1c1793754fdf83a33fe7b1b34c.
| -rw-r--r-- | printing/miscprint.ml | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/printing/miscprint.ml b/printing/miscprint.ml index 1fbf703f5b..7b2c5695fd 100644 --- a/printing/miscprint.ml +++ b/printing/miscprint.ml @@ -36,16 +36,9 @@ 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 -> - 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 "]" + str "[" ++ + hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) + ++ str "]" (** Printing of [move_location] *) |