Sebastian Ullrich
|
36189cb51a
|
chore: simplify parser cache key computation, panic on environment/token table divergence
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
ed03ff9d00
|
perf: cache leading_parser and syntax as well
We better hope the `leading_parser`s are closed terms
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
da6efe1bca
|
fix: make parser caching sound (I hope?)
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
35509b5e98
|
refactor: more sensible ordering of declarations in Lean.Parser.Basic
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
246923886a
|
fix: do not create choice nodes for failed parses
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
57320712f0
|
fix: extraneous missing items on parser stack
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
7e193a45ce
|
perf: cache category parses
|
2022-11-11 09:13:02 +01:00 |
|
Leonardo de Moura
|
2386c401d2
|
chore: use String.get' and String.next' at Parser/Basic.lean
This commit also cleans up old frontend legacy.
|
2022-11-09 17:06:22 -08:00 |
|
Adrien Champion
|
5849fdc6c9
|
feat: require strict indentation on nested by-s
|
2022-11-08 08:30:42 -08:00 |
|
Mario Carneiro
|
4bf89dfa12
|
feat: allow doSeq in let x <- e | seq
fixes #1804
|
2022-11-08 08:29:21 -08:00 |
|
Mario Carneiro
|
32b6bd0d8b
|
feat: empty type ascription syntax (e :) (part 2)
|
2022-11-07 19:10:56 +01:00 |
|
Mario Carneiro
|
02d8a5d56e
|
feat: empty type ascription syntax (e :)
|
2022-11-07 19:10:56 +01:00 |
|
Sebastian Ullrich
|
5249611d75
|
doc: fix mkAntiquot docstring
|
2022-11-03 10:07:38 +01:00 |
|
Mario Carneiro
|
9b40613207
|
fix: formatting for if let and do if
|
2022-11-01 20:19:39 -07:00 |
|
Sebastian Ullrich
|
7475fd9cbd
|
feat: ignore patternIgnore nodes in syntax patterns
|
2022-10-28 21:25:47 +02:00 |
|
Mario Carneiro
|
29bda62198
|
fix: missed a file from #1771
|
2022-10-27 11:14:13 -07:00 |
|
Leonardo de Moura
|
e369c3beb6
|
fix: disallow . immediately after ..
Rejects the following weird example
```
```
which was being parsed as
```
```
|
2022-10-26 07:13:40 -07:00 |
|
Leonardo de Moura
|
00ca0dde5c
|
feat: add unop% term parser
We not to support unary minus at `BinOp.toTree`
see #1779
|
2022-10-26 06:19:22 -07:00 |
|
Mario Carneiro
|
d7d61bfb55
|
feat: use withoutPosition consistently (part 2)
|
2022-10-24 12:51:32 -07:00 |
|
Mario Carneiro
|
765ebcdbf0
|
feat: use withoutPosition consistently
|
2022-10-24 12:51:32 -07:00 |
|
Mario Carneiro
|
e7c7678ab0
|
refactor: line wrapping in parser code
|
2022-10-24 08:37:29 -07:00 |
|
Mario Carneiro
|
b3ba78aade
|
feat: hovers & name resolution in registerCombinatorAttribute (part 2)
|
2022-10-23 09:30:38 +02:00 |
|
Mario Carneiro
|
583e023314
|
chore: snake-case attributes (part 2)
|
2022-10-19 09:28:08 -07:00 |
|
Mario Carneiro
|
dd5948d641
|
chore: snake-case attributes (part 1)
|
2022-10-19 09:28:08 -07:00 |
|
Gabriel Ebner
|
fb4d90a58b
|
feat: dynamic quotations for categories
|
2022-10-18 14:59:14 -07:00 |
|
Mario Carneiro
|
faa612e7b7
|
chore: remove #resolve_name
|
2022-10-17 14:53:51 -07:00 |
|
Mario Carneiro
|
c06cffa54f
|
refactor: rename isExitCommand -> isTerminalCommand
|
2022-10-12 11:11:31 -07:00 |
|
Mario Carneiro
|
8dfae9eb38
|
feat: import command stub
|
2022-10-12 11:11:31 -07:00 |
|
Gabriel Ebner
|
0d3d05bd3a
|
feat: clear%
|
2022-10-11 17:24:35 -07:00 |
|
Mario Carneiro
|
391aef5cd7
|
feat: automatic extension names
|
2022-10-06 17:19:30 -07:00 |
|
Sebastian Ullrich
|
71e647049f
|
refactor: lexOrd should not be an instance
|
2022-09-28 15:57:01 -07:00 |
|
Sebastian Ullrich
|
d0a002ffff
|
fix: prefer longer parse even if unsuccessful
|
2022-09-28 15:57:01 -07:00 |
|
Mario Carneiro
|
85119ba9d1
|
chore: move Std.* data structures to Lean.*
|
2022-09-26 05:46:04 -07:00 |
|
Gabriel Ebner
|
a351a4be70
|
feat: use colEq in sepByIndent
|
2022-09-19 12:44:43 -07:00 |
|
Gabriel Ebner
|
b1bef71d59
|
feat: colEq parser
|
2022-09-19 12:44:43 -07:00 |
|
Gabriel Ebner
|
ee9c9b1312
|
feat: skip final newline in sepByIndent format
|
2022-09-18 16:43:23 -07:00 |
|
Gabriel Ebner
|
7356840cbc
|
feat: use sepBy1Indent for tactic blocks
|
2022-09-18 16:43:23 -07:00 |
|
Mario Carneiro
|
6392c5b456
|
chore: import reductions
|
2022-09-15 14:02:38 -07:00 |
|
Gabriel Ebner
|
f1b5fa53f0
|
chore: use new comment syntax
|
2022-09-14 08:26:17 -07:00 |
|
Gabriel Ebner
|
59abb9a332
|
feat: move docstring before | in ctors
|
2022-09-14 08:26:17 -07:00 |
|
Gabriel Ebner
|
54e7d31d0f
|
feat: allow empty whereStructInst
|
2022-09-13 06:19:40 -07:00 |
|
Mario Carneiro
|
3bb3efdedc
|
feat: allow optional type in example
|
2022-09-13 03:11:04 -07:00 |
|
Sebastian Ullrich
|
2770b9e98b
|
chore: inheritDoc misbehaves on built-in parsers
|
2022-09-13 03:08:23 -07:00 |
|
Sebastian Ullrich
|
a4ac7087dc
|
doc: some do extensions
|
2022-09-13 03:08:23 -07:00 |
|
Leonardo de Moura
|
e39c3af5bb
|
chore: remove [inline] from parser combinators
|
2022-09-08 14:50:27 -07:00 |
|
Leonardo de Moura
|
f611a6e52f
|
feat: add specialize attribute parser
|
2022-09-07 14:50:29 -07:00 |
|
Sebastian Ullrich
|
a657a638f0
|
feat: sub-info tree level hover
|
2022-08-31 17:49:43 -07:00 |
|
Sebastian Ullrich
|
4050227e5d
|
chore: revert marking internal notes as parser/elab docstrings
|
2022-08-31 17:49:43 -07:00 |
|
Sebastian Ullrich
|
fb408c024b
|
fix: deleting built-in docstrings
|
2022-08-27 17:19:25 +02:00 |
|
Gabriel Ebner
|
82e9f09bca
|
fix: remove incorrect syntax coercion
|
2022-08-25 17:54:26 +02:00 |
|