diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-04 18:06:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-14 12:49:22 +0200 |
| commit | d50923b778684a2ffcc211beb5341a54304c97a4 (patch) | |
| tree | 9f4b57ed2b7ba4eb420caa02af0a020dfe346f5f /interp/constrextern.mli | |
| parent | f4cec75fe74ff3f66f401efab357cae79124d984 (diff) | |
[print] Allow Selective Printing of Notations
We add new API to the printer to allows toggling the printing of
individual notations and scopes:
```ocaml
val toggle_scope_printing :
scope:Notation_term.scope_name -> activate:bool -> unit
val toggle_notation_printing :
?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit
```
This API is meant to be used by ML plugins.
[this commit includes some refactoring by EJGA]
Diffstat (limited to 'interp/constrextern.mli')
| -rw-r--r-- | interp/constrextern.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index ea627cff1..d771ee86f 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -80,3 +80,13 @@ val without_specific_symbols : interp_rule list -> ('a -> 'b) -> 'a -> 'b (** This prints metas as anonymous holes *) val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b + +(** Fine-grained activation and deactivation of notation printing. + *) +val toggle_scope_printing : + scope:Notation_term.scope_name -> activate:bool -> unit + +val toggle_notation_printing : + ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit + + |