aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/notation_term.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-06-26 18:40:11 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-07-26 15:03:31 +0200
commitada7875e95cba2f08902c55cfd3f69d6cc80cac3 (patch)
treef989fe34a04bfc803f5bd6449a198bd9558ee116 /intf/notation_term.ml
parent51d418636adf30bcf4e37a5b7b479a7d54dbedb2 (diff)
Adding support for recursive notations of the form "x , .. , y , z".
Since camlp5 parses from left, the last ", z" was parsed as part of an arbitrary long list of "x1 , .. , xn" and a syntax error was raised since an extra ", z" was still expected. We support this by translating "x , .. , y , z" into "x , y , .. , z" and reassembling the arguments appropriately after parsing.
Diffstat (limited to 'intf/notation_term.ml')
-rw-r--r--intf/notation_term.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 0fa0afdad..cee96040b 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -83,9 +83,10 @@ type notation_interp_env = {
type grammar_constr_prod_item =
| GramConstrTerminal of Tok.t
| GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option
- | GramConstrListMark of int * bool
+ | GramConstrListMark of int * bool * int
(* tells action rule to make a list of the n previous parsed items;
- concat with last parsed list if true *)
+ concat with last parsed list when true; additionally release
+ the p last items as if they were parsed autonomously *)
type notation_grammar = {
notgram_level : int;