Sebastian Ullrich
|
d7a0197fee
|
chore: improve tacticSeqIndentGt error message
|
2023-03-15 10:52:57 +01:00 |
|
Gabriel Ebner
|
181fbdfb42
|
feat: add fun x ↦ y syntax
|
2023-01-03 13:59:53 -08:00 |
|
Gabriel Ebner
|
e71a2e58bb
|
fix: remove misleading leading space in " where"
|
2022-12-21 22:54:42 +01:00 |
|
Gabriel Ebner
|
0d598dcfdf
|
fix: Format.align always prints whitespace
|
2022-12-21 22:54:42 +01:00 |
|
Sebastian Ullrich
|
96ccf192e8
|
fix: parenthesize by optParam values
|
2022-12-20 18:10:39 +01:00 |
|
Sebastian Ullrich
|
4c11743f4b
|
refactor: split paren parser, part 2
|
2022-11-11 13:45:41 +01:00 |
|
Sebastian Ullrich
|
791fc70dd9
|
refactor: split paren parser
|
2022-11-11 13:45:41 +01:00 |
|
Sebastian Ullrich
|
d5255e94e8
|
perf: improve dynamicQuot caching
|
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 |
|
Adrien Champion
|
5849fdc6c9
|
feat: require strict indentation on nested by-s
|
2022-11-08 08:30:42 -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 |
|
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
|
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 |
|
Gabriel Ebner
|
0d3d05bd3a
|
feat: clear%
|
2022-10-11 17:24:35 -07:00 |
|
Gabriel Ebner
|
7356840cbc
|
feat: use sepBy1Indent for tactic blocks
|
2022-09-18 16:43:23 -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 |
|
Gabriel Ebner
|
82e9f09bca
|
fix: remove incorrect syntax coercion
|
2022-08-25 17:54:26 +02:00 |
|
Mario Carneiro
|
014db5d6d0
|
doc: relocate doc strings from elab to syntax
|
2022-08-13 17:16:40 -07:00 |
|
Mario Carneiro
|
b0db7deeef
|
doc: documentation for Init.Coe
|
2022-08-13 17:15:49 -07:00 |
|
Mario Carneiro
|
e816424466
|
chore: use Category declarations for builtin cats too (#1400)
|
2022-08-03 18:10:54 -07:00 |
|
Leonardo de Moura
|
e39eebabd9
|
fix: move doc string to parser that sets the SyntaxNodeKind for the { tac } notation
see #1403
This fixes the hover for `{ tac }`
|
2022-08-01 13:01:37 -07:00 |
|
Leonardo de Moura
|
2f00d60115
|
feat: helper parser for issue #1371
|
2022-07-31 04:30:02 -07:00 |
|
Mario Carneiro
|
9a401c852c
|
feat: add decl_name% / with_decl_name% macros
|
2022-07-29 21:42:51 +02:00 |
|
Leonardo de Moura
|
1bf53e4fc9
|
doc: add doc strings for let parsers
|
2022-07-27 10:56:44 -07:00 |
|
Mario Carneiro
|
f6211b1a74
|
chore: convert doc/mod comments from /- to /--//-! (#1354)
|
2022-07-22 12:05:31 -07:00 |
|
Leonardo de Moura
|
fd371ea812
|
chore: remove getOp builtin support
|
2022-07-09 16:04:17 -07:00 |
|
Sebastian Ullrich
|
d7bcc271be
|
refactor: avoid nested sequence in simpleBinder
|
2022-07-08 19:06:10 +02:00 |
|
Leonardo de Moura
|
131e7be8c5
|
feat: add a[i]? and a[i]! parsers
|
2022-07-02 07:29:58 -07:00 |
|
Sebastian Ullrich
|
f90e4ae30c
|
feat: more TSyntax API & coercions
|
2022-06-27 22:37:02 +02:00 |
|
Sebastian Ullrich
|
c202a2c013
|
feat: more antiquotation kinds
|
2022-06-27 22:37:02 +02:00 |
|
Sebastian Ullrich
|
2c54a0d17a
|
feat: allow anonymous antiquotations for tacticSeq
|
2022-06-27 22:37:02 +02:00 |
|
Sebastian Ullrich
|
3b3961a89b
|
chore: disable some anonymous antiquotations
|
2022-06-27 22:37:02 +02:00 |
|
Sebastian Ullrich
|
292d24ba19
|
feat: always store quoted kind in antiquotation kind
|
2022-06-27 22:37:02 +02:00 |
|
Gabriel Ebner
|
ec4200fc75
|
chore: remove unnecessary ppLine
|
2022-06-24 10:59:55 +02:00 |
|
Sebastian Ullrich
|
4212cc740b
|
refactor: move linebreak check into sepBy(1)Indent
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
|
2022-06-16 23:33:57 +02:00 |
|
Sebastian Ullrich
|
ce054fb2e7
|
fix: introduce semicolonOrLinebreak, replace many(1) with sepBy(1) where appropriate
|
2022-06-16 23:33:57 +02:00 |
|
Sebastian Ullrich
|
392640d292
|
feat: allow keyword-like projection identifiers
|
2022-05-10 12:25:30 -07:00 |
|
Leonardo de Moura
|
8d9626dab7
|
feat: delaborate match h : d with ...
|
2022-04-29 07:17:46 -07:00 |
|
Sebastian Ullrich
|
3cf2afa42e
|
refactor: clean up parsers using withAnonymousAntiquot := false
|
2022-04-06 10:21:53 +02:00 |
|
Sebastian Ullrich
|
ffee6676ef
|
feat: allow adjusting anonymous antiquot generation at leading_parser
|
2022-04-06 10:21:53 +02:00 |
|
Leonardo de Moura
|
eae4b92b0d
|
feat: use sorry if failed to synthesize default element for unsafe constant
|
2022-04-05 16:52:54 -07:00 |
|
Leonardo de Moura
|
8f4d58893f
|
feat: update match parser
Support for
```
def fib (x : Nat) : Nat :=
match x with
| 0 | 1 => 1
| x+2 => fib (x+1) + fib x
```
TODO: expand `matchAlts`
|
2022-03-20 13:22:39 -07:00 |
|