- !rule_id @ pp_id
- | Interpretation (loc, dsc, l2, l3) ->
- let interp_id = Interpretations.add_interpretation dsc l2 l3 in
- [InterpretationId interp_id]
- | st -> []
-
-let remove_notation = function
- | RuleId id ->
- let item =
- try
- Hashtbl.find !rule_ids_to_items id
- with Not_found -> assert false in
- RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id)
- !parser_ref_counter item
- | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
- | InterpretationId id -> Interpretations.remove_interpretation id
-
-let get_all_notations () =
- List.map
- (fun (interp_id, dsc) ->
- InterpretationId interp_id, "interpretation: " ^ dsc)
- (Interpretations.get_all_interpretations ())
-
-let get_active_notations () =
- List.map (fun id -> InterpretationId id)
- (Interpretations.get_active_interpretations ())
-
-let set_active_notations ids =
- let interp_ids =
- HExtlib.filter_map
- (function InterpretationId interp_id -> Some interp_id | _ -> None)
- ids
- in
- Interpretations.set_active_interpretations interp_ids
-
-let history = ref [];;
-
-let push () =
- history := (!parser_ref_counter,!rule_ids_to_items) :: !history;
- parser_ref_counter := initial_parser_ref_counter ();
- rule_ids_to_items := initial_rule_ids_to_items ();
- TermContentPres.push ();
- Interpretations.push ();
- CicNotationParser.push ()
-;;