Leonardo de Moura
e021a7d011
chore: remove symbolNoWs
...
@Kha This is a leftover from the time precedence was associated with
tokens instead of parsers.
2020-10-09 16:17:56 -07:00
Sebastian Ullrich
21f1a66ceb
feat: add & use ppDedent parser combinator
2020-10-07 09:46:47 +02:00
Sebastian Ullrich
5d76a981b0
chore: adjust pp spacing
2020-10-07 09:44:04 +02:00
Leonardo de Moura
5c74c408ae
chore: remove nodeSepBy1Unbox combinator
2020-10-06 08:28:40 -07:00
Leonardo de Moura
9a551d9219
feat: add withForbidden and withoutForbidden parser combinators
2020-10-05 09:36:28 -07:00
Leonardo de Moura
2755972447
fix: missing checkColGt and tests
2020-09-28 17:10:59 -07:00
Leonardo de Moura
f45fa34cba
feat: optional ; at tacticSeq1Indented
2020-09-28 17:10:59 -07:00
Leonardo de Moura
1fcdbaf223
feat: add withoutPosition combinator
2020-09-28 17:10:57 -07:00
Leonardo de Moura
6ddec22763
refactor: simplify withPosition combinator
...
Add `checkColGt`
2020-09-28 17:10:56 -07:00
Leonardo de Moura
453ce9b3b8
feat: add eoi parser
2020-09-27 16:54:19 -07:00
Leonardo de Moura
e31fd665f0
feat: add checkLineLe parser
2020-09-26 14:03:28 -07:00
Leonardo de Moura
a1579f3123
fix: notFollowedBy info
2020-09-26 12:33:11 -07:00
Leonardo de Moura
dc9626ceab
feat: try to improve weird error message
...
@Kha Before this commit, we were producing the error "expected command" at the `let` token
```lean
check id let x := 1; x
```
The new error is "expected command, but found term; this error may be
due to parsing precedence levels, consider parenthesizing the term".
The example above looks artificial, but it will happen all the time as
users start to define their own notation.
2020-09-21 18:29:01 -07:00
Leonardo de Moura
9eb978946c
chore: add quotedCharCoreFn
2020-09-20 17:05:47 -07:00
Leonardo de Moura
fe2d3be821
feat: parser priorities
2020-09-19 17:55:17 -07:00
Sebastian Ullrich
68568e78d3
feat: formatter: use hard space after opening structure instance brace
2020-09-18 13:15:40 -07:00
Sebastian Ullrich
95007171a8
feat: formatter: group+indent binders and structure instance fields
2020-09-18 13:15:40 -07:00
Leonardo de Moura
d1c3ab3797
feat: many1Unbox and nodeSepBy1Unbox parser combinators
...
@Kha I removed the dummy parenthesizer/formatter for `withResultOf`,
and add proper ones for `many1Unbox` and `nodeSepBy1Unbox`.
2020-09-17 13:17:46 -07:00
Leonardo de Moura
2dafdec000
feat: use withResultOf combinator instead of unboxSingleton parameter
2020-09-17 12:12:12 -07:00
Leonardo de Moura
4265348bed
feat: add withResultOf parser combinator and unboxSingleton
2020-09-17 12:03:16 -07:00
Sebastian Ullrich
fad4660135
feat: pretty print space between binders
2020-09-17 08:12:28 -07:00
Leonardo de Moura
3c2044f06b
chore: add coercion for new frontend
2020-09-13 10:12:25 -07:00
Leonardo de Moura
2563d03ae2
feat: add notFollowedBy
2020-08-31 15:37:41 -07:00
Sebastian Ullrich
3091bd71e7
feat: unwrap basic token parsers
2020-08-19 09:56:23 -07:00
Sebastian Ullrich
d4952dc40b
feat: use insideQuot parsers
2020-08-19 09:56:23 -07:00
Sebastian Ullrich
ed7edf5661
feat: add checkInsideQuot/checkOutsideQuot/toggleInsideQuot parsers
...
One use case is to obtain fine-grained control over at what stage changed syntax is activated
2020-08-19 09:56:23 -07:00
Sebastian Ullrich
46f5670ba3
chore: Lean.Parser.Parser ~> Lean.Parser.Basic
2020-08-13 18:44:13 +02:00
