Sebastian Ullrich
fb408c024b
fix: deleting built-in docstrings
2022-08-27 17:19:25 +02:00
Mario Carneiro
59b32da2d9
feat: go to def on parser aliases
2022-08-06 12:44:14 +02:00
Mario Carneiro
e816424466
chore: use Category declarations for builtin cats too ( #1400 )
2022-08-03 18:10:54 -07:00
Mario Carneiro
ecb787529a
refactor: rename ref to declName
2022-08-01 11:23:09 +02:00
Mario Carneiro
711532f5c6
feat: add ref field to ParserCategory
2022-08-01 11:23:09 +02:00
Mario Carneiro
65e2b8a932
feat: track parser names by category
2022-08-01 11:23:09 +02:00
Mario Carneiro
603b7486e3
feat: add go-to-def for simple attributes
2022-07-31 16:36:54 +02:00
Sebastian Ullrich
6a767a66a1
perf: reduce Lean.Parser.Basic imports
2022-07-23 23:01:52 +02:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
Sebastian Ullrich
5d187b8beb
fix: register tokens in parser quotation
2022-07-21 23:49:57 +02:00
Gabriel Ebner
a8cab84735
refactor: use computed fields for Expr
2022-07-11 14:19:41 -07:00
Sebastian Ullrich
eab64997cd
fix: auto-group syntax parsers where necessary
2022-06-28 11:50:59 +02:00
Sebastian Ullrich
7d48d125da
fix: store syntax kinds of parser aliases in order to construct correct antiquotations in macro and elab
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
Leonardo de Moura
d56163bd0e
refactor: resolveNamespace now return a List
2022-06-16 17:16:36 -07:00
Leonardo de Moura
02c4e548df
feat: replace constant with opaque
2022-06-14 17:02:59 -07:00
Leonardo de Moura
041827bed5
chore: unused variables
2022-06-07 17:54:10 -07:00
Sebastian Ullrich
ae7b895f7a
refactor: unname some unused variables
2022-06-07 16:37:45 -07:00
Sebastian Ullrich
0a39e9cbdc
fix: dynamic quotations should use previous stage by default
...
@leodemoura as discussed some time ago
2022-05-25 09:46:10 +02:00
Sebastian Ullrich
e1fbc04c3b
chore: accept unregistered syntax kinds in stage 1
2022-04-15 08:50:46 -07:00
Sebastian Ullrich
24697026e8
feat: always accept antiquotations, simplify quotDepth code
2022-04-06 19:43:07 +02:00
Sebastian Ullrich
e10e664cc1
chore: typos
2022-04-06 10:21:53 +02:00
Leonardo de Moura
fdd1cb5751
chore: remove workarounds for #1090
2022-04-01 11:28:17 -07:00
Leonardo de Moura
09de67780f
chore: prepare for #1090
2022-04-01 09:35:06 -07:00
Leonardo de Moura
12e2a79170
chore: fix codebase after removing auto pure
2022-02-03 18:08:14 -08:00
Leonardo de Moura
cf3b8d4eb4
chore: cleanup
...
Make the code style more uniform.
We still have a lot of leftovers from the old frontend.
2022-01-26 09:18:17 -08:00
Gabriel Ebner
7e483d3a0a
feat: support syntax abbreviations in dynamic quotations
2021-12-15 11:17:58 +00:00
Leonardo de Moura
68bd55af32
chore: fix codebase
2021-12-10 13:12:09 -08:00
Sebastian Ullrich
2a1aee2b7a
feat: record declaration ranges of builtin parsers & elaborators
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
e9f7c88299
feat: record doc strings of builtin parsers & elaborators
2021-11-26 17:13:19 +01:00
Sebastian Ullrich
8176084dcf
refactor: factor out declareBuiltin
2021-11-26 17:13:19 +01:00
Leonardo de Moura
79e6732fc6
fix: update tokenTable at withNamespace parser combinator
...
It also moves `withOpen` and `withOpenDecl` applications to simplify
their definitions and make sure we do not need to reset the cache.
2021-08-23 09:41:36 -07:00
Leonardo de Moura
d93c4317d1
feat: add withOpenDecl and withOpen parsers
...
It allow us to process `open .. in ..` while parsing.
This is useful for activating a scoped parser while parsing.
TODO: `openOnly` and `openHiding`, these two cases are rarely used
with `open .. in ..`
closes #529
2021-08-22 20:50:35 -07:00
Leonardo de Moura
c913886938
chore: add private annotations
2021-08-03 18:15:39 -07:00
Leonardo de Moura
bba9353619
fix: make sure isDefEqOffset does not expose kernel nat literals
...
This issue is similar to a bug where `isDefEqOffset` was exposing
`Nat.add` when processing `HAdd.hAdd`.
Fixes #561
The example at issue #561 is now working, but we may have other places
where raw literals are being accidentally exposed.
2021-08-02 11:27:00 -07:00
Sebastian Ullrich
73cf3533a1
fix: count quotation depth in parser correctly
2021-04-29 13:33:48 +02:00
Sebastian Ullrich
725c0c1911
chore: implement lhs prec
2021-03-22 16:33:37 +01:00
Sebastian Ullrich
9f21d6fd64
fix: preserve token parse errors
2021-03-14 08:23:32 -07:00
Leonardo de Moura
be841a7cad
chore: throwError! => throwError, throwErrorAt! => throwErrorAt
...
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
2021-03-11 11:59:45 -08:00
Leonardo de Moura
ea0fda39bc
chore: Declaration.lean naming convention
...
`Declaration.lean` was one of the first Lean 4 files, and was still
using an old naming convention.
cc @Kha
2021-01-20 17:07:02 -08:00
Leonardo de Moura
f0ac477d2e
feat: add sanity checks
2021-01-01 18:31:28 -08:00
Leonardo de Moura
0083e1996a
fix: scoped tokens
...
Tokens introduced by scoped (local) parsers should be scoped (local).
2020-12-21 13:11:09 -08:00
Sebastian Ullrich
4380d4a9da
feat: parser: store options & pass to evalConst
2020-12-16 23:15:58 +01:00
Leonardo de Moura
ed87480093
refactor: move to attr syntax category
2020-12-15 20:22:04 -08:00
Leonardo de Moura
6100ed9283
feat: add LeadingIdentBehavior type
...
Different strategies for handling the leading identifier in the
`Pratt` parser loop.
2020-12-15 16:45:14 -08:00
Leonardo de Moura
9e3b3b2495
refactor: move attribute related parsers to separate file
2020-12-15 16:13:11 -08:00
Sebastian Ullrich
314c5c9d41
feat: run single non-category quotation under interpreter as well
2020-12-14 17:13:59 +01:00
Sebastian Ullrich
a9bdb2f70a
feat: prefer interpreter for running builtin parsers in quotations
2020-12-14 16:45:32 +01:00
Leonardo de Moura
3b6d65c3c3
chore: use deriving Inhabited
2020-12-13 10:09:20 -08:00
Sebastian Ullrich
4dfa7e1187
feat: use actual separator in sepBy antiquotation scope
2020-12-09 17:48:05 +01:00
