| _, RuleId _ -> 1
| x,y -> Pervasives.compare x y
-let parser_ref_counter = RefCounter.create ()
-let rule_ids_to_items = Hashtbl.create 113
+let initial_parser_ref_counter () = RefCounter.create ()
+let initial_rule_ids_to_items ()= Hashtbl.create 113
+
+let parser_ref_counter = ref (initial_parser_ref_counter ());;
+let rule_ids_to_items = ref (initial_rule_ids_to_items ());;
let process_notation st =
match st with
| Notation (loc, dir, l1, associativity, precedence, l2) ->
let l1 =
- CicNotationParser.check_l1_pattern l1 precedence associativity
+ CicNotationParser.check_l1_pattern
+ l1 (dir = Some `RightToLeft) precedence associativity
in
let item = (l1, precedence, associativity, l2) in
let rule_id = ref [] in
CicNotationPt.AttributedTerm
(`Loc loc,TermContentPres.instantiate_level2 env l2)) in
rule_id := [ RuleId id ];
- Hashtbl.add rule_ids_to_items id item
+ Hashtbl.add !rule_ids_to_items id item
in
- RefCounter.incr ~create_cb parser_ref_counter item
+ RefCounter.incr ~create_cb !parser_ref_counter item
in
let pp_id =
if dir <> Some `LeftToRight then
| RuleId id ->
let item =
try
- Hashtbl.find rule_ids_to_items id
+ 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
+ !parser_ref_counter item
| PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
| InterpretationId id -> TermAcicContent.remove_interpretation id
in
TermAcicContent.set_active_interpretations interp_ids
-let reset () =
- TermContentPres.reset ();
- TermAcicContent.reset ()
+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 ();
+ TermAcicContent.push ();
+ CicNotationParser.push ()
+;;
+
+let pop () =
+ TermContentPres.pop ();
+ TermAcicContent.pop ();
+ CicNotationParser.pop ();
+ match !history with
+ | [] -> assert false
+ | (prc,riti) :: tail ->
+ parser_ref_counter := prc;
+ rule_ids_to_items := riti;
+ history := tail;
;;