+class type g_status =
+ object
+ method notation_parser_db: db
+ end
+
+class status0 ~keywords:kwds =
+ object
+ val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] }
+ method notation_parser_db = db
+ method set_notation_parser_db v = {< db = v >}
+ method set_notation_parser_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> {< db = o#notation_parser_db >}
+ end
+
+class virtual status ~keywords:kwds =
+ object
+ inherit NCic.status
+ inherit status0 kwds
+ end
+
+let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
+ (* move inside constructor XXX *)
+ let add1item status (level, level1_pattern, action) =
+ let p_bindings, p_atoms =
+ List.split (extract_term_production status level1_pattern) in
+ Grammar.extend
+ [ Grammar.Entry.obj
+ (status#notation_parser_db.grammars.term : 'a Grammar.Entry.e),
+ Some (Gramext.Level level),
+ [ None,
+ Some (*Gramext.NonA*) Gramext.NonA,
+ [ p_atoms,
+ (make_action
+ (fun (env: NotationEnv.t) (loc: Ast.location) ->
+ (action env loc))
+ p_bindings) ]]];
+ status
+ in
+ let current_item =
+ let level = level_of precedence in
+ level, level1_pattern, action in
+ let keywords = NotationUtil.keywords_of_term level1_pattern @
+ status#notation_parser_db.keywords in
+ let items = current_item :: status#notation_parser_db.items in
+ let status = status#set_notation_parser_status (new status0 ~keywords) in
+ let status = status#set_notation_parser_db
+ {status#notation_parser_db with items = items} in
+ List.fold_left add1item status items