Leonardo de Moura
93090baa82
chore: cleanup tactic syntax
2020-09-28 17:10:57 -07:00
Leonardo de Moura
96a0fb41be
feat: optional ; in do notation
2020-09-28 17:10:57 -07:00
Leonardo de Moura
08d54b6043
feat: add checkColGt at app
...
@Kha Only one example broke :)
2020-09-28 17:10:57 -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
39f8fd8eb9
fix: trailing ';' at end of input
2020-09-27 16:58:23 -07:00
Leonardo de Moura
453ce9b3b8
feat: add eoi parser
2020-09-27 16:54:19 -07:00
Leonardo de Moura
7dcd011be0
chore: improve notFollowedBy at doExpr
...
cc @Kha
2020-09-27 06:59:43 -07:00
Leonardo de Moura
2d4b7e7952
feat: add doMatch parser
2020-09-27 06:29:21 -07:00
Leonardo de Moura
8f27848d82
chore: preparing for "reassignment" notation
2020-09-26 18:16:35 -07:00
Leonardo de Moura
5fa8d9105e
feat: add if and for for do blocks
2020-09-26 18:03:53 -07:00
Leonardo de Moura
0275d23ad7
fix: ignore $ at notFollowedByCategoryToken when inside quotations
2020-09-26 17:57:26 -07:00
Leonardo de Moura
ee4dc452ac
chore: remove leftover
2020-09-26 16:10:29 -07:00
Leonardo de Moura
6892a957d6
feat: trailing ; in indented "do" sequences
...
cc @Kha
2020-09-26 16:08:30 -07:00
Leonardo de Moura
3d6cc2de08
feat: add notFollowedByCategoryToken parser
2020-09-26 15:53:23 -07:00
Leonardo de Moura
3f4499be08
feat: allow trailing ; at doSeqBracketed
2020-09-26 14:20:47 -07:00
Leonardo de Moura
e31fd665f0
feat: add checkLineLe parser
2020-09-26 14:03:28 -07:00
Leonardo de Moura
13ded3f964
chore: use doElem category
2020-09-26 12:51:24 -07:00
Leonardo de Moura
a1579f3123
fix: notFollowedBy info
2020-09-26 12:33:11 -07:00
Leonardo de Moura
2d8506b7c6
feat: add doElem parser category
2020-09-26 06:18:44 -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
b0564a32b9
feat: add AttrM
...
We are going to use `AttrM` to implement solution 2 described at https://github.com/leanprover/lean4/issues/175
2020-09-21 16:44:20 -07:00
Leonardo de Moura
cab56d1e1b
chore: do not invoke the hooks from addImported
...
@Kha I am working on issue
https://github.com/leanprover/lean4/issues/175
I am using solution 2 described there. The hooks will be at `AttrM`
instead of `CoreM`.
AFAICT code deleted by this commit is not necessary.
2020-09-21 16:28:07 -07:00
Sebastian Ullrich
f693e910b1
fix: skip minimum amount of tokens during parser recovery
...
Fixes #186
2020-09-21 11:37:50 +02:00
Leonardo de Moura
9eb978946c
chore: add quotedCharCoreFn
2020-09-20 17:05:47 -07:00
Leonardo de Moura
03a361edf4
feat: add initialize command parser
2020-09-20 13:42:50 -07:00
Leonardo de Moura
87381e3329
feat: add support for parser priorities in the syntax command
...
@Kha Parser priorities are working :)
2020-09-19 18:47:08 -07:00
Leonardo de Moura
f0ab743ad0
chore: remove temporary workaround
2020-09-19 18:00:45 -07:00
Leonardo de Moura
fe2d3be821
feat: parser priorities
2020-09-19 17:55:17 -07:00
Leonardo de Moura
f679b7d803
feat: add notFollowedBy to syntax
2020-09-19 15:43:44 -07:00
Leonardo de Moura
ee6d723554
feat: add stx.quot
2020-09-19 14:40:17 -07:00
Leonardo de Moura
f876177f26
feat: expand macros in syntax declaration
2020-09-19 14:39:49 -07:00
Leonardo de Moura
17d4117637
chore: remove temporary hacks
2020-09-19 14:21:38 -07:00
Leonardo de Moura
71de0c8eb9
chore: rename category syntax to stx
...
Reason: `syntax` is a keywork. So, we can't write `macro "boo" x:syntax`
2020-09-19 14:11:35 -07:00
Leonardo de Moura
caa624c936
chore: cleanup
2020-09-19 09:24:50 -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
8142548237
fix: missing toggleInsideQuot
...
cc @Kha
2020-09-17 13:23:52 -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
Leonardo de Moura
56f8103e66
chore: improve error message for rw []
2020-09-17 10:55:51 -07:00
Leonardo de Moura
9d1f2b644f
chore: rwRuleSeq ; => ,
2020-09-17 08:15:58 -07:00
Sebastian Ullrich
0b9e46eee5
chore: universe-+ spacing
2020-09-17 08:12:28 -07:00
Sebastian Ullrich
fad4660135
feat: pretty print space between binders
2020-09-17 08:12:28 -07:00
Sebastian Ullrich
c4761974b7
fix: runParserCategory: ensure EOI
2020-09-17 08:12:28 -07:00
Leonardo de Moura
a2e8a41f33
feat: rewrite tactic parser
2020-09-16 17:43:44 -07:00
Leonardo de Moura
c620a2a59d
feat: refine parser location
2020-09-16 17:28:09 -07:00
Leonardo de Moura
0abca5475f
refactor: move ppExpr to IO
...
@Kha I am also tracking `currNamespace` and `openDecls`.
BTW, I also tried an experiment where I added `currNamespace` and
`openDecls` to `Meta.Context`, but it looked weird. This information
is only needed in the elaborator and pretty printer.
The `PPContext` object should contain everything you need. You
can put `currNamespace` and `openDecls` in the `Delaborator.Context`.
2020-09-15 18:48:21 -07:00
Leonardo de Moura
3fa7e61b26
feat: add done and admit syntax
2020-09-15 10:46:40 -07:00
