diff options
| author | Enrico Tassi | 2014-09-24 17:37:10 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-09-29 21:54:31 +0200 |
| commit | 8f118b444db7693dcc16dda4c271d2528bfa949a (patch) | |
| tree | a01df0fd808a3d17b1e3d12d7710225c533bfe12 /interp/notation.mli | |
| parent | ec49447d078da25959d617ae23e55a668fdd1646 (diff) | |
Notation: option to attach extra pretty printing rules to notations
so that one can retrieve them and pass them to third party tools (i.e.
print the AST with the notations attached to the nodes concerned).
Available syntax:
- all in one:
Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2").
- a posteriori:
Format Notation "a /\ b" "latex" "#1 \wedge #2".
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 95e176064c..961e1e12ea 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -185,8 +185,12 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd (** Declare and look for the printing rule for symbolic notations *) type unparsing_rule = unparsing list * precedence -val declare_notation_printing_rule : notation -> unparsing_rule -> unit +type extra_unparsing_rules = (string * string) list +val declare_notation_printing_rule : + notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit val find_notation_printing_rule : notation -> unparsing_rule +val find_notation_extra_printing_rules : notation -> extra_unparsing_rules +val add_notation_extra_printing_rule : notation -> string -> string -> unit (** Rem: printing rules for primitive token are canonical *) |