diff options
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 24 |
1 files changed, 7 insertions, 17 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e0cdc1b62..7c1f05cd3 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -479,14 +479,6 @@ let make_hunks etyps symbols from = in make symbols -let rec trailing_precedence etyps from = function - | [] -> assert false - | [NonTerminal id|SProdList (id,_)] -> - let typ = List.assoc id etyps in - Some (precedence_of_entry_type from typ) - | [Terminal _|Break _] -> None - | _ :: l -> trailing_precedence etyps from l - (* Build default printing rules from explicit format *) let error_format () = error "The format does not match the notation." @@ -680,7 +672,7 @@ type syntax_extension = { synext_level : Notation.level; synext_notation : notation; synext_notgram : notation_grammar; - synext_unparsing : unparsing_rule; + synext_unparsing : unparsing list; synext_extra : (string * string) list; } @@ -699,7 +691,7 @@ let cache_one_syntax_extension se = Egramcoq.extend_constr_grammar prec se.synext_notgram; (* Declare the printing rule *) Notation.declare_notation_printing_rule ntn - ~extra:se.synext_extra se.synext_unparsing + ~extra:se.synext_extra (se.synext_unparsing, fst prec) let cache_syntax_extension (_, (_, sy)) = List.iter cache_one_syntax_extension sy @@ -1059,7 +1051,7 @@ exception NoSyntaxRule let recover_syntax ntn = try let prec = Notation.level_of_notation ntn in - let pp_rule= Notation.find_notation_printing_rule ntn in + let pp_rule,_ = Notation.find_notation_printing_rule ntn in let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in let pa_rule = Egramcoq.recover_constr_grammar ntn prec in { synext_level = prec; @@ -1093,16 +1085,14 @@ let make_pa_rule i_typs (n,typs,symbols,_) ntn = notgram_prods = prod; notgram_typs = i_typs; } -let make_pp_rule (n,typs,symbols,fmt) (lev,_) = - let unp = match fmt with +let make_pp_rule (n,typs,symbols,fmt) = + match fmt with | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)] - | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt) in - let trailingprec = trailing_precedence typs lev symbols in - (unp, lev, trailingprec) + | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt) let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra = let pa_rule = make_pa_rule i_typs sy_data ntn in - let pp_rule = make_pp_rule sy_data prec in + let pp_rule = make_pp_rule sy_data in let sy = { synext_level = prec; synext_notation = ntn; |