diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-13 10:10:51 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-13 18:13:21 +0200 |
| commit | dea5e12a1828c58b2349e89b95eee6ba633c6cc9 (patch) | |
| tree | 40ac939f23ce27d2f6b25d176b8e88d020718167 /parsing | |
| parent | 7cfcaa57a68ea9abde9e2558ceef86589aa26d6d (diff) | |
Parsing of "?[" as two tokens (makes ssr compile).
The problem is that "?[" makes the lexer glue "?" and "[" into
a single token but in ssr "?" (iteration) and "[" (rewrite pattern
delimiter) are often close, but they are parsed by very hard to
refactor grammar entries.
To consider:
- check the adjacency of the two symbols looking at the loc to
parse exactly the same sentences as before this patch
- change syntax completely, e.g. "(_ as id)"
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 49c0cd79c..ebf603111 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -289,8 +289,8 @@ GEXTEND Gram | n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n)) | s=string -> CPrim (!@loc, String s) | "_" -> CHole (!@loc, None, IntroAnonymous, None) - | "?["; id=ident; "]" -> CHole (!@loc, None, IntroIdentifier id, None) - | "?["; id=pattern_ident; "]" -> CHole (!@loc, None, IntroFresh id, None) + | "?"; "["; id=ident; "]" -> CHole (!@loc, None, IntroIdentifier id, None) + | "?"; "["; id=pattern_ident; "]" -> CHole (!@loc, None, IntroFresh id, None) | id=pattern_ident; inst = evar_instance -> CEvar(!@loc,id,inst) ] ] ; inst: |