diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-09 15:12:20 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-09 15:12:20 +0200 |
| commit | a82c30c08c7442b6bb43829d2be6a299f493ca88 (patch) | |
| tree | fc4ee6e5e395c94d15d2b7109ee00c7372b5a31d /vernac/metasyntax.ml | |
| parent | c3f7302e9f6849298bbb34dc91516751444888ff (diff) | |
| parent | f1531b5deb0f2bbb5653bb6f02abf6a1896f399a (diff) | |
Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 5298ef2e4..b2d48bb2f 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -991,7 +991,7 @@ let is_not_printable onlyparse nonreversible = function (warn_non_reversible_notation (); true) else onlyparse -let find_precedence lev etyps symbols = +let find_precedence lev etyps symbols onlyprint = let first_symbol = let rec aux = function | Break _ :: t -> aux t @@ -1009,8 +1009,13 @@ let find_precedence lev etyps symbols = | None -> [],0 | Some (NonTerminal x) -> (try match List.assoc x etyps with - | ETConstr _ -> - user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") + | ETConstr _ -> + if onlyprint then + if Option.is_empty lev then + user_err Pp.(str "Explicit level needed in only-printing mode when the level of the leftmost non-terminal is given.") + else [],Option.get lev + else + user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") | ETName | ETBigint | ETReference -> begin match lev with | None -> @@ -1134,7 +1139,7 @@ let compute_syntax_data df modifiers = let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in let ntn_for_grammar = if need_squash then make_notation_key symbols_for_grammar else ntn_for_interp in if not onlyprint then check_rule_productivity symbols_for_grammar; - let msgs,n = find_precedence mods.level mods.etyps symbols in + let msgs,n = find_precedence mods.level mods.etyps symbols onlyprint in (* To globalize... *) let etyps = join_auxiliary_recursive_types recvars mods.etyps in let sy_typs, prec = |