diff options
| author | Georges Gonthier | 2019-05-21 16:50:17 +0200 |
|---|---|---|
| committer | Georges Gonthier | 2019-05-23 18:38:48 +0200 |
| commit | 7c82a2713c8827ebc1e2896c83c6e7bd2f81c063 (patch) | |
| tree | 6119746e0f4f791a19be114bdfaa2f2ae67748a8 /printing | |
| parent | 6dadcffd83b034c177d1e8d2153b51e306138333 (diff) | |
do not parse `|` as infix in patterns; parse `|}` as `|` `}`
* use mixfix `(p1 | … | pn)` notation for nested disjunctive patterns,
rather than infix `|`, making pattern syntax consistent with term
syntax.
* disable extending `pattern` grammar with notation incompatible with
the nested disjunctive pattern syntax `(p1 | … | pn)`, such as the `(p
| q)` divisibility notation used by `Numbers`.
* emit a (disabled by default) `disj-pattern-notation` warning when such
`Notation` is attempted.
* update documentation accordingly; document incompatibilities in
`changelog`.
* comment special treatment of `(num)` in grammar.
* update file extensions in `Pcoq` header comment.
* correct the keyword declarations to reflect the contents of the
grammar files; perhaps there should be an option to disable implicit
keyword extension in a `.mlg` file, so that these lists could actually
be checked.
* parse the `|}` manifest record terminator as `|` followed by `}`,
eliminating the `|}` token which conflicts with notations that use `|`
as a terminator (such as, absolute value, norm, or cardinal in
MathComp). Since `|` is now an `operconstr` _and_ `pattern` terminator,
`bar_cbrace` rule checks for contiguous symbols, this change entails no
visible behaviour change.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 9d3ed40f6c..e2a63a4540 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -249,7 +249,7 @@ let tag_var = tag Tag.variable str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) let las = lapp - let lpator = 100 + let lpator = 0 let lpatrec = 0 let rec pr_patt sep inh p = @@ -283,7 +283,8 @@ let tag_var = tag Tag.variable pr_reference r, latom | CPatOr pl -> - hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator + let pp = pr_patt mt (lpator,Any) in + surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator | CPatNotation ((_,"( _ )"),([p],[]),[]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom |