diff options
Diffstat (limited to 'parsing/egrammar.ml')
| -rw-r--r-- | parsing/egrammar.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 1793be4134..74b275fabf 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -111,23 +111,28 @@ let make_constr_prod_item univ assoc from forpat = function let eobj = symbol_of_production assoc from forpat nt in (eobj, ovar) +let prepare_empty_levels entry (pos,p4assoc,name,reinit) = + grammar_extend entry pos reinit [(name, p4assoc, [])] + let extend_constr entry (n,assoc,pos,p4assoc,name,reinit) mkact (forpat,pt) = let univ = get_univ "constr" in let pil = List.map (make_constr_prod_item univ assoc n forpat) pt in let (symbs,ntl) = List.split pil in + let needed_levels = register_empty_levels forpat symbs in + List.iter (prepare_empty_levels entry) needed_levels; grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact ntl])] let extend_constr_notation (n,assoc,ntn,rule) = (* Add the notation in constr *) let mkact loc env = CNotation (loc,ntn,List.map snd env) in - let (e,level,keepassoc) = get_constr_entry false (ETConstr (n,())) in - let pos,p4assoc,name,reinit = find_position false keepassoc assoc level in + let (e,level) = get_constr_entry false (ETConstr (n,())) in + let pos,p4assoc,name,reinit = find_position false assoc level in extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name,reinit) (make_constr_action mkact) (false,rule); (* Add the notation in cases_pattern *) let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in - let (e,level,keepassoc) = get_constr_entry true (ETConstr (n,())) in - let pos,p4assoc,name,reinit = find_position true keepassoc assoc level in + let (e,level) = get_constr_entry true (ETConstr (n,())) in + let pos,p4assoc,name,reinit = find_position true assoc level in extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name,reinit) (make_cases_pattern_action mkact) (true,rule) @@ -265,7 +270,7 @@ let add_tactic_entry (key,lev,prods,tac) = let mkact s tac loc l = (TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in make_rule univ (mkact key tac) mkprod prods in - let _ = find_position true true None None (* to synchronise with remove *) in + synchronize_level_positions (); grammar_extend entry pos None [(None, None, List.rev [rules])] (**********************************************************************) |