Sebastian Ullrich
|
241430aa03
|
perf: avoid calculating position, revert building unexpected message in mkUnexpectedTokenErrors
|
2023-09-12 11:42:24 +02:00 |
|
Sebastian Ullrich
|
c67686132a
|
feat: include unexpected token in error message
|
2023-09-12 11:42:24 +02:00 |
|
Sebastian Ullrich
|
e580c903e6
|
feat: adjust message range on unexpected token error
|
2023-09-12 11:42:24 +02:00 |
|
Sebastian Ullrich
|
6c0baf4aed
|
feat: support reporting range for parser errors, report ranges for expected token errors
|
2023-09-12 11:42:24 +02:00 |
|
Sebastian Ullrich
|
f4fc8b3e15
|
refactor: parser error setters
|
2023-09-12 11:42:24 +02:00 |
|
Mario Carneiro
|
2037094f8c
|
doc: document all parser aliases (#2499)
|
2023-09-06 09:02:25 +00:00 |
|
Marcus Rossel
|
7ee7595637
|
doc: fix typos (#2467)
|
2023-08-28 15:40:33 +10:00 |
|
Sebastian Ullrich
|
8fc1af650a
|
fix: symmetry in orelse antiquotation parsing
|
2023-07-28 08:36:33 -07:00 |
|
Sebastian Ullrich
|
eceac9f12a
|
perf: avoid syntax stack copy at orelseFn
|
2023-07-28 08:36:33 -07:00 |
|
Mario Carneiro
|
2348fb37d3
|
fix: use Lean.initializing instead of IO.initializing
|
2023-06-17 06:57:14 -07:00 |
|
Mario Carneiro
|
e64a2e1a12
|
fix: misleading indentation
|
2023-06-17 06:56:53 -07:00 |
|
Mario Carneiro
|
b139a97825
|
fix: hygieneInfo should not consume whitespace
|
2023-06-09 15:05:19 +02:00 |
|
Mario Carneiro
|
43f6d0a761
|
feat: implement have this (part 1)
|
2023-06-02 16:19:02 +02:00 |
|
Mario Carneiro
|
c20a7bf305
|
feat: hygieneInfo parser (aka this 2.0)
|
2023-06-02 16:19:02 +02:00 |
|
Mario Carneiro
|
5661b15e35
|
fix: spacing and indentation fixes
|
2023-05-28 18:48:36 -07:00 |
|
Mario Carneiro
|
df49512880
|
fix: use withoutPosition in anon constructor
|
2023-05-17 09:48:34 +02:00 |
|
Sebastian Ullrich
|
a89accfbbe
|
feat: parser alias for tacticSeqIndentGt
|
2023-03-15 10:54:05 +01:00 |
|
Sebastian Ullrich
|
d7a0197fee
|
chore: improve tacticSeqIndentGt error message
|
2023-03-15 10:52:57 +01:00 |
|
Sebastian Ullrich
|
f24608c4d1
|
fix: make eoi an actual command with info tree
|
2023-01-26 13:05:57 +01:00 |
|
Leonardo de Moura
|
6fea2946c2
|
fix: fixes #2006
|
2023-01-04 08:19:22 -08: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
|
9c9cc017df
|
fix: ignore empty character literals
|
2022-12-12 22:59:06 +01:00 |
|
Mario Carneiro
|
17ef0cea8a
|
feat: intra-line withPosition formatting
|
2022-11-28 09:02:08 -08:00 |
|
Sebastian Ullrich
|
07953062ed
|
perf: remove unnecessary, cache-defeating withPosition in doReassignArrow
|
2022-11-28 08:14:03 -08:00 |
|
Sebastian Ullrich
|
42a080fae2
|
fix: comments ending in --/
Fixes #1883
|
2022-11-25 10:32:49 +01:00 |
|
Leonardo de Moura
|
a7107aedb3
|
fix: fixes #1848
|
2022-11-18 08:49:10 -08:00 |
|
Sebastian Ullrich
|
1f447efa54
|
doc: update Lean.Parser.Basic
|
2022-11-11 14:17:21 +01:00 |
|
Sebastian Ullrich
|
7cdd8f81d7
|
refactor: simplify withCacheFn
|
2022-11-11 14:07:15 +01:00 |
|
Sebastian Ullrich
|
43767f8f35
|
fix: uncacheable syntax stack access in doIf
|
2022-11-11 13:45:41 +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
|
30dd28480d
|
fix: suppressInsideQuot inside quotation
|
2022-11-11 13:45:41 +01:00 |
|
Sebastian Ullrich
|
0dea086669
|
fix: reset lhsPrec, errorMsg in withCacheFn
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
22510db004
|
refactor: simplify parser code using withFn
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
e7bf1cd3dc
|
refactor: simplify adaptUncacheableContextFn
compiler.ir.result reports 0 allocations on happy path
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
fb941d0827
|
fix: ensure parser caching is sound re. syntax stack accesses
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
12b267bd8c
|
refactor: categoryParserOfStack is dead
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
17782fba1a
|
fix: replace broken ptrEq cache sanity checks with private ParserContext constructor
The context is now manipulated using `adaptCacheableContext` and `adaptUncacheableContext`
and created using `ParserFn.run`.
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
d5255e94e8
|
perf: improve dynamicQuot caching
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
d3f7d0350f
|
refactor: move parser types into separate file
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
9a4626c495
|
fix: must cache stack of parser evals
|
2022-11-11 09:13:02 +01:00 |
|
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 |
|