diff options
| -rw-r--r-- | parsing/egrammar.ml | 44 | ||||
| -rw-r--r-- | parsing/extend.ml | 1 | ||||
| -rw-r--r-- | parsing/g_basevernac.ml4 | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 13 | ||||
| -rw-r--r-- | toplevel/metasyntax.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
6 files changed, 33 insertions, 31 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 5b57774920..17d9736211 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -47,22 +47,25 @@ let symbolic_level = function | 11 -> "pattern", None | n -> "constr", Some n -let numeric_levels = ref [8;1;0] - -exception Found - -let find_position n = - let after = ref 8 in - let rec add_level q = function - | p::l when p > n -> p :: add_level p l - | p::l when p = n -> raise Found - | l -> after := q; n::l - in - try - numeric_levels := add_level 8 !numeric_levels; - Gramext.After (constr_level !after) - with - Found -> Gramext.Level (constr_level n) +let numeric_levels = + ref [8,Some Gramext.RightA; 1,None; 0,None ] + +exception Found of Gramext.g_assoc option + +let find_position assoc = function + | None -> None, assoc + | Some n -> + let after = ref 8 in + let rec add_level q = function + | (p,_ as pa)::l when p > n -> pa :: add_level p l + | (p,a)::l when p = n -> raise (Found a) + | l -> after := q; (n,assoc)::l + in + try + numeric_levels := add_level 8 !numeric_levels; + Some (Gramext.After (constr_level !after)), assoc + with + Found a -> Some (Gramext.Level (constr_level n)), a (* Interpretation of the right hand side of grammar rules *) @@ -179,7 +182,7 @@ let extend_entry univ (te, etyp, pos, name, ass, rls) = let define_entry univ {ge_name=n; gl_assoc=ass; gl_rules=rls} = let typ = explicitize_entry (fst univ) n in let e,lev = entry_of_type true typ in - let pos = option_app find_position lev in + let pos,ass = find_position ass lev in let name = option_app constr_level lev in (e,typ,pos,name,ass,rls) @@ -216,19 +219,16 @@ let extend_constr entry pos (level,assoc) make_act pt = let act = make_act ntl in grammar_extend entry pos [(level, assoc, [symbs, act])] -let constr_entry name = - object_of_typed_entry (get_entry (get_univ "constr") name) - let extend_constr_notation (n,assoc,ntn,rule) = let mkact loc env = CNotation (loc,ntn,env) in let (e,level) = entry_of_type false (ETConstr ((n,Ppextend.E),Some n)) in - let pos = option_app find_position level in + let pos,assoc = find_position assoc level in extend_constr e pos (option_app constr_level level,assoc) (make_act mkact) rule let extend_constr_delimiters (sc,rule,pat_rule) = let mkact loc env = CDelimiters (loc,sc,snd (List.hd env)) in - extend_constr (constr_entry "constr") (Some (Gramext.Level "top")) + extend_constr Constr.constr (Some (Gramext.Level "0")) (None,None) (make_act mkact) rule; let mkact loc env = CPatDelimiters (loc,sc,snd (List.hd env)) in diff --git a/parsing/extend.ml b/parsing/extend.ml index 2e4eea4b0f..70704f0195 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -162,6 +162,7 @@ let explicitize_entry univ nt = | "constr8" | "constr" -> ETConstr ((8,E),Some 8) | "constr9" -> ETConstr ((9,E),Some 9) | "constr10" | "lconstr" -> ETConstr ((10,E),Some 10) + | "pattern" -> ETPattern | "ident" -> ETIdent | "global" -> ETReference | _ -> ETOther (univ,nt) diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index d042f8c915..4d675a0828 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -226,7 +226,7 @@ GEXTEND Gram | IDENT "Open"; IDENT "Scope"; sc = IDENT -> VernacOpenScope sc | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> - VernacDelimiters (sc,("'"^key^":","'")) + VernacDelimiters (sc,key) | IDENT "Arguments"; IDENT "Scope"; qid = global; "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 858add3c78..8efa576f0d 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -662,13 +662,14 @@ let (inDelim,outDelim) = load_function = load_delimiters; export_function = (fun x -> Some x) } -let make_delimiter_rule (l,r) typ = +let make_delimiter_rule key typ = let e = Nameops.make_ident "e" None in - let symbols = [Terminal l; NonTerminal e; Terminal r] in + let m = key^":" in + let symbols = [Terminal "`"; Terminal m; NonTerminal e; Terminal "`"] in make_production [e,typ] symbols -let add_delimiters scope (l,r as dlms) = - if l = "" or r = "" then error "Delimiters cannot be empty"; - let gram_rule = make_delimiter_rule dlms (ETConstr ((0,E),Some 0)) in - let pat_gram_rule = make_delimiter_rule dlms ETPattern in +let add_delimiters scope key = + let gram_rule = make_delimiter_rule key (ETConstr ((0,E),Some 0)) in + let pat_gram_rule = make_delimiter_rule key ETPattern in + let dlms = ("`"^key^":", "`") in Lib.add_anonymous_leaf (inDelim(gram_rule,pat_gram_rule,scope,dlms)) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index fbbe4a94e5..a63d1dea91 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -34,7 +34,7 @@ val add_infix : val add_distfix : grammar_associativity -> precedence -> string -> reference -> scope_name option -> unit -val add_delimiters : scope_name -> delimiters -> unit +val add_delimiters : scope_name -> string -> unit val add_notation : string -> constr_expr -> syntax_modifier list -> scope_name option -> unit diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 050ac58d1c..6076184b8d 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -155,7 +155,7 @@ type vernac_expr = | VernacSyntax of string * raw_syntax_entry list | VernacSyntaxExtension of string * syntax_modifier list | VernacOpenScope of scope_name - | VernacDelimiters of scope_name * (string * string) + | VernacDelimiters of scope_name * string | VernacArgumentsScope of reference * scope_name option list | VernacInfix of grammar_associativity * precedence * string * reference * |