diff options
| author | Hugo Herbelin | 2019-09-29 00:06:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-19 21:09:07 +0100 |
| commit | 039b2423cf7b85f2f5960dde6a1586f0f07cf9d0 (patch) | |
| tree | 1fe4fd03177b52af4dd0e3a4f04b92fedd93ae71 /parsing/ppextend.mli | |
| parent | 9dc88f3c146aeaf8151fcef6ac45ca50675d052b (diff) | |
Addressing #6082 and #7766 (overriding format of notation).
We do two changes:
- We distinguish between a notion of format generically attached to
notations and a new notion of format attached to interpreted
notations. "Reserved Notation" attaches a format
generically. "Notation" attaches the format specifically to the given
interpretation, and additionally, attaches it generically if it is the
first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
a specific format.
Diffstat (limited to 'parsing/ppextend.mli')
| -rw-r--r-- | parsing/ppextend.mli | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli index be5af75e72..7996e7696d 100644 --- a/parsing/ppextend.mli +++ b/parsing/ppextend.mli @@ -41,11 +41,14 @@ type unparsing = type unparsing_rule = unparsing list * precedence type extra_unparsing_rules = (string * string) list -val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit -val find_notation_printing_rule : notation -> unparsing_rule -val find_notation_extra_printing_rules : notation -> extra_unparsing_rules -val find_notation_parsing_rules : notation -> notation_grammar -val add_notation_extra_printing_rule : notation -> string -> string -> unit -(** Returns notations with defined parsing/printing rules *) -val get_defined_notations : unit -> notation list +val unparsing_eq : unparsing -> unparsing -> bool + +val declare_generic_notation_printing_rules : notation -> reserved:bool -> extra:extra_unparsing_rules -> unparsing_rule -> unit +val declare_specific_notation_printing_rules : specific_notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit +val has_generic_notation_printing_rule : notation -> bool +val find_generic_notation_printing_rule : notation -> unparsing_rule * bool * extra_unparsing_rules +val find_specific_notation_printing_rule : specific_notation -> unparsing_rule * extra_unparsing_rules +val find_notation_printing_rule : notation_with_optional_scope option -> notation -> unparsing_rule +val find_notation_extra_printing_rules : notation_with_optional_scope option -> notation -> extra_unparsing_rules +val add_notation_extra_printing_rule : notation -> string -> string -> unit |