X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.mli;h=f587291aa5452e006dfc25c54c216eeba0e09c31;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=6516061389218313208b470f182daf687f3b6cc0;hpb=98d5d40127827a5c40e58cb0c9654066f940b0ea;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli index 651606138..f587291aa 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.mli +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -28,7 +28,7 @@ val ast_of_acic: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> (* id -> sort *) Cic.annterm -> (* acic *) CicNotationPt.term (* ast *) - * (Cic.id, string) Hashtbl.t (* id -> uri *) + * (Cic.id, UriManager.uri) Hashtbl.t (* id -> uri *) (** level 2 -> level 1 *) val pp_ast: CicNotationPt.term -> CicNotationPt.term @@ -66,3 +66,9 @@ val remove_interpretation: interpretation_id -> unit (** @raise Pretty_printer_not_found *) val remove_pretty_printer: pretty_printer_id -> unit +(** {2 Interpretations toggling} *) + +val get_all_interpretations: unit -> (interpretation_id * string) list +val get_active_interpretations: unit -> interpretation_id list +val set_active_interpretations: interpretation_id list -> unit +