| Ast.Magic m -> aux_magic m
| Ast.Variable v -> aux_variable v
| t ->
- prerr_endline (NotationPp.pp_term t);
+ prerr_endline (NotationPp.pp_term status t);
assert false
and aux_literal =
function
exc_located_wrapper
(fun () -> Grammar.Entry.parse grammars.level2_meta (Obj.magic lexbuf))
-let parse_term grammars lexbuf =
- exc_located_wrapper
- (fun () -> (Grammar.Entry.parse grammars.term (Obj.magic lexbuf)))
-
(* create empty precedence level for "term" *)
let initialize_grammars grammars =
let dummy_action =
in
let rec find_arg name n = function
| [] ->
+ (* CSC: new NCicPp.status is the best I can do here
+ without changing the return type *)
Ast.fail loc (sprintf "Argument %s not found"
- (NotationPp.pp_term name))
+ (NotationPp.pp_term (new NCicPp.status) name))
| (l,_) :: tl ->
(match position_of name 0 l with
| None, len -> find_arg name (n + len) tl
method notation_parser_db: db
end
-class status ~keywords:kwds =
+class status0 ~keywords:kwds =
object
val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] }
method notation_parser_db = db
= 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 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 status ~keywords) 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
parse_level2_ast status#notation_parser_db.grammars
let parse_level2_meta status =
parse_level2_meta status#notation_parser_db.grammars
-let parse_term status =
- parse_term status#notation_parser_db.grammars
let level2_ast_grammar status =
status#notation_parser_db.grammars.level2_ast_grammar