diff options
| author | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
| commit | 1965c3e4a1f3ab4ab8a777fe3707e71891bac162 (patch) | |
| tree | 5c8266aa94cc1097b18535eda4ef9eb40ea21249 | |
| parent | 1cf1fb46904d149a4f8e597735ed4fb1b4ff24d3 (diff) | |
Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"
This reverts commit fd8669f9f2e37607f5eba56ba25e267711876e62.
| -rw-r--r-- | printing/miscprint.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/printing/miscprint.ml b/printing/miscprint.ml index 1ab6cc8b90..1fbf703f5b 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] *) |