diff options
| author | Pierre-Marie Pédrot | 2016-01-16 14:57:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-16 15:41:40 +0100 |
| commit | 8a3b19b62720e2324ef24003407c2e83335a51a5 (patch) | |
| tree | 08ba41c4192143e277fa518bebb4da4d1c981b69 /intf | |
| parent | 3914cc110faeb67c399dda0791a600bad7b7ef31 (diff) | |
Separating the parsing of user-defined entries from their intepretation.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/extend.mli | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/intf/extend.mli b/intf/extend.mli index 975f194b07..651fa638b5 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -51,6 +51,18 @@ type constr_prod_entry_key = type simple_constr_prod_entry_key = (production_level,unit) constr_entry_key_gen +(** {5 AST for user-provided entries} *) + +type user_symbol = +| Ulist1 : user_symbol -> user_symbol +| Ulist1sep : user_symbol * string -> user_symbol +| Ulist0 : user_symbol -> user_symbol +| Ulist0sep : user_symbol * string -> user_symbol +| Uopt : user_symbol -> user_symbol +| Umodifiers : user_symbol -> user_symbol +| Uentry : string -> user_symbol +| Uentryl : string * int -> user_symbol + (** {5 Type-safe grammar extension} *) type ('self, 'a) symbol = |