+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
+;;
+
+