diff options
| author | Emilio Jesus Gallego Arias | 2017-06-04 18:06:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-14 12:49:22 +0200 |
| commit | d50923b778684a2ffcc211beb5341a54304c97a4 (patch) | |
| tree | 9f4b57ed2b7ba4eb420caa02af0a020dfe346f5f /API/API.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 'API/API.mli')
0 files changed, 0 insertions, 0 deletions