(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
-(** level 1 -> level 0: see CicNotationPres.render *)
+ (** for level 1 -> level 0: see CicNotationPres.render *)
type interpretation_id
type pretty_printer_id
val add_interpretation:
- string -> (* id / description *)
+ string -> (* id / description *)
string * CicNotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
- CicNotationPt.cic_appl_pattern -> (* level 3 pattern *)
+ CicNotationPt.cic_appl_pattern -> (* level 3 pattern *)
interpretation_id
(** @raise Interpretation_not_found *)
val add_pretty_printer:
precedence:int ->
associativity:Gramext.g_assoc ->
- CicNotationPt.term -> (* level 2 pattern *)
- CicNotationPt.term -> (* level 1 pattern *)
+ CicNotationPt.term -> (* level 2 pattern *)
+ CicNotationPt.term -> (* level 1 pattern *)
pretty_printer_id
exception Interpretation_not_found
(** @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
+