From d50923b778684a2ffcc211beb5341a54304c97a4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 4 Jun 2017 18:06:26 +0200 Subject: [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] --- interp/constrextern.mli | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'interp/constrextern.mli') 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 + + -- cgit v1.2.3