| Age | Commit message (Collapse) | Author |
|---|
|
Instead of just string (and empty strings for tokens without payload)
|
|
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")
|
|
In this way one can also set the current offsets in a file,
useful if you are parsing a Coq fragment within a file instead
of a full file starting from the first line.
|
|
This is useless in the functorial API.
|
|
The types are identical and we have no more reason for the split. Note
the following TODOS:
- discrepancy of `Ploc.after` with `CLexer.after`
- discrepancy of `Ploc.comments` with `CLexer.comments`
- `Ploc.dummy` vs `Loc.t option`
|
|
|
|
- remove duplicate type definitions `gram_assoc`, `gram_position`,
- make global `warning_verbose` variable into a parameter.
|
|
|
|
No effect on actual code.
|
|
|
|
This constructor only makes sense in the backtracking mode, that has
been removed from our vendored version of camlp5.
|
|
It is just a wrapper around Sopt. I do not really understand why it is
hardwired in the entry AST.
|
|
Used by rule factorisation in theory, but appears to be unused in Coq.
|
|
It is only used in strict mode, which makes no sense for Coq grammar.
|
|
We remove the functional and backtracking parsers as they are not used
in Coq.
|
|
`for i in *; do camlp5r pr_o.cmo $i > ../gramlib.auto/$i; done`
|
|
|
