type notation_id =
| RuleId of CicNotationParser.rule_id
- | InterpretationId of TermAcicContent.interpretation_id
+ | InterpretationId of Interpretations.interpretation_id
| PrettyPrinterId of TermContentPres.pretty_printer_id
+class type g_status =
+ object ('self)
+ inherit Interpretations.g_status
+ inherit TermContentPres.g_status
+ end
+
+class status =
+ object (self)
+ inherit Interpretations.status
+ inherit TermContentPres.status
+ method set_notation_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> (self#set_interp_status o)#set_content_pres_status o
+ end
+
let compare_notation_id x y =
match x,y with
| RuleId i1, RuleId i2 -> CicNotationParser.compare_rule_id i1 i2
let parser_ref_counter = ref (initial_parser_ref_counter ());;
let rule_ids_to_items = ref (initial_rule_ids_to_items ());;
-let process_notation st =
+let process_notation status st =
match st with
| Notation (loc, dir, l1, associativity, precedence, l2) ->
let l1 =
let id =
CicNotationParser.extend l1
(fun env loc ->
- CicNotationPt.AttributedTerm
+ NotationPt.AttributedTerm
(`Loc loc,TermContentPres.instantiate_level2 env l2)) in
rule_id := [ RuleId id ];
Hashtbl.add !rule_ids_to_items id item
in
RefCounter.incr ~create_cb !parser_ref_counter item
in
- let pp_id =
+ let status,pp_id =
if dir <> Some `LeftToRight then
- [ PrettyPrinterId
- (TermContentPres.add_pretty_printer
- l2 l1) ]
+ let status,id = TermContentPres.add_pretty_printer status l2 l1 in
+ status,[ PrettyPrinterId id ]
else
- []
+ status,[]
in
- !rule_id @ pp_id
+ status,!rule_id @ pp_id
| Interpretation (loc, dsc, l2, l3) ->
- let interp_id = TermAcicContent.add_interpretation dsc l2 l3 in
- [InterpretationId interp_id]
- | st -> []
+ let status,interp_id =
+ Interpretations.add_interpretation status dsc l2 l3
+ in
+ status,[InterpretationId interp_id]
+ | st -> status,[]
let remove_notation = function
| RuleId 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 -> TermAcicContent.remove_interpretation id
-
-let get_all_notations () =
- List.map
- (fun (interp_id, dsc) ->
- InterpretationId interp_id, "interpretation: " ^ dsc)
- (TermAcicContent.get_all_interpretations ())
-
-let get_active_notations () =
- List.map (fun id -> InterpretationId id)
- (TermAcicContent.get_active_interpretations ())
-
-let set_active_notations ids =
- let interp_ids =
- HExtlib.filter_map
- (function InterpretationId interp_id -> Some interp_id | _ -> None)
- ids
- in
- TermAcicContent.set_active_interpretations interp_ids
+ | PrettyPrinterId id -> ()
+ | InterpretationId id -> ()
let history = ref [];;
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 ();
- TermAcicContent.push ();
CicNotationParser.push ()
;;
let pop () =
- TermContentPres.pop ();
- TermAcicContent.pop ();
CicNotationParser.pop ();
match !history with
| [] -> assert false