diff options
| author | Enrico Tassi | 2019-03-05 11:42:17 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-03-31 14:36:28 +0200 |
| commit | 912eaf40d4efd29b7e3489d51c55b8b79206df79 (patch) | |
| tree | b4793da97a5513d460c3d08721cb40692eeddd71 /gramlib/plexing.mli | |
| parent | ed996432fd079583afbb1797c92ad23f654b94eb (diff) | |
[parsing] Split Tok.t into Tok.t and Tok.pattern
Tokens were having a double role:
- the output of the lexer
- the items of grammar entries, especially terminals
Now tokens are the output of the lexer, and this paves the way for
using a richer data type, eg including Loc.t
Patterns, as in Plexing.pattern, only represent patterns (for tokens)
and now have a bit more structure (eg the wildcard is represented
as None, not as "", while a regular pattern for "x" as Some "x")
Diffstat (limited to 'gramlib/plexing.mli')
| -rw-r--r-- | gramlib/plexing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli index f6e4d96b80..48722e01be 100644 --- a/gramlib/plexing.mli +++ b/gramlib/plexing.mli @@ -8,7 +8,7 @@ grammars (see module [Grammar]). It also provides some useful functions to create lexers. *) -type pattern = string * string +type pattern = string * string option (* Type for values used by the generated code of the EXTEND statement to represent terminals in entry rules. - The first string is the constructor name (must start with |