| InterpretationId of TermAcicContent.interpretation_id
| PrettyPrinterId of TermContentPres.pretty_printer_id
+let compare_notation_id x y =
+ match x,y with
+ | RuleId i1, RuleId i2 -> CicNotationParser.compare_rule_id i1 i2
+ | RuleId _, _ -> ~-1
+ | _, RuleId _ -> 1
+ | x,y -> Pervasives.compare x y
+
let parser_ref_counter = RefCounter.create ()
let rule_ids_to_items = Hashtbl.create 113
let process_notation st =
match st with
| Notation (loc, dir, l1, associativity, precedence, l2) ->
+ let l1 =
+ CicNotationParser.check_l1_pattern l1 precedence associativity
+ in
let item = (l1, precedence, associativity, l2) in
let rule_id = ref [] in
let _ =
if dir <> Some `RightToLeft then
let create_cb (l1, precedence, associativity, l2) =
let id =
- CicNotationParser.extend l1 ?precedence ?associativity
+ CicNotationParser.extend l1
(fun env loc ->
CicNotationPt.AttributedTerm
(`Loc loc,TermContentPres.instantiate_level2 env l2)) in
let pp_id =
if dir <> Some `LeftToRight then
[ PrettyPrinterId
- (TermContentPres.add_pretty_printer ?precedence ?associativity
+ (TermContentPres.add_pretty_printer
l2 l1) ]
else
[]
in
TermAcicContent.set_active_interpretations interp_ids
+let reset () =
+ TermContentPres.reset ();
+ TermAcicContent.reset ()
+;;