diff options
| author | Hugo Herbelin | 2016-04-16 16:18:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:47 +0200 |
| commit | fd8669f9f2e37607f5eba56ba25e267711876e62 (patch) | |
| tree | 50520ef2bce57adf1110a3600ad8c9bb6eba5fa3 | |
| parent | 0d56fda01ecf8b38ef5f9a1fd3552f025972fbcd (diff) | |
Revert "Protect printing of intro-patterns from collision when "[|" or
"|]"" because this commit triggers a
Error: Files proofs/proofs.cma(Miscprint)
and /usr/local/lib/ocaml/compiler-libs/ocamlcommon.cma(Lexer)
make inconsistent assumptions over interface Lexer
Adding two extra spaces systematically instead.
This reverts commit 72be1f6beafafc3edd30df673fbb6c7e88f8fac7.
| -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..1ab6cc8b90 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] *) |