Wojciech Nawrocki
|
eef413cec8
|
chore: unused binding in FromToJson
|
2021-07-15 21:57:55 +02:00 |
|
Mario Carneiro
|
c7f5fd6ce4
|
fix: missing interpolation in trace message
|
2021-07-15 10:32:37 +02:00 |
|
Mario Carneiro
|
8d616e060b
|
doc: fix categoryParenthesizer documentation
|
2021-07-15 09:39:28 +02:00 |
|
Daniel Fabian
|
0d41fd03f7
|
feat: add xml parser.
in order to generate the LLVM extern declarations we want to use a generator that spits out XML. Hence adding a small XML parser.
|
2021-07-13 09:58:27 -07:00 |
|
Wojciech Nawrocki
|
521ed11330
|
chore: move parseTagged
It should live in Lean.Data.Json.FromToJson because many modules import that but not Lean.Elab.Deriving.FromToJson.
|
2021-07-12 09:10:29 +02:00 |
|
Sebastian Ullrich
|
0839ead35e
|
perf: server: avoid redundant publishDiagnostics
This should reduce server & editor load for the common case where most
command do *not* emit diagnostics
|
2021-07-08 12:12:19 +02:00 |
|
Wojciech Nawrocki
|
1ba802418b
|
fix: ToJson for single-field constructors
|
2021-07-08 09:01:06 +02:00 |
|
Wojciech Nawrocki
|
6ca8389670
|
fix: preserve synthetic positions in sanitizer
|
2021-07-06 09:29:23 +02:00 |
|
Wojciech Nawrocki
|
fd9e3d8fe6
|
chore: add completion test and go-to field type
|
2021-07-05 19:42:01 +02:00 |
|
Wojciech Nawrocki
|
dfcdc57302
|
feat: go-to for structure fields
|
2021-07-05 19:42:01 +02:00 |
|
Wojciech Nawrocki
|
24dcdad832
|
feat: check prefix in option completion
|
2021-07-05 19:42:01 +02:00 |
|
Wojciech Nawrocki
|
522cbc16d9
|
fix: typo
|
2021-07-05 19:42:01 +02:00 |
|
Wojciech Nawrocki
|
c7beb283e9
|
feat: allow requests to log to stderr
|
2021-07-05 19:42:01 +02:00 |
|
Leonardo de Moura
|
5e694d4b69
|
fix: fixes #536
|
2021-06-29 18:24:46 -07:00 |
|
Leonardo de Moura
|
f4a7ffd8c8
|
chore: fix codebase and tests
|
2021-06-29 17:14:52 -07:00 |
|
Leonardo de Moura
|
90a79a0b06
|
chore: remove command universes
Now, `universe` may declare many universes. The goal is to make it
consistent with the `variable` command
|
2021-06-29 17:01:07 -07:00 |
|
Leonardo de Moura
|
e9b78585c5
|
refactor: add BuiltinCommand.lean
|
2021-06-29 16:52:00 -07:00 |
|
Leonardo de Moura
|
818efe719e
|
fix: fixes #533
|
2021-06-29 15:20:46 -07:00 |
|
Leonardo de Moura
|
2018dc0959
|
fix: disable panic messages during initialization
This is a temporary workaround until we implement #467.
Fixes #534
|
2021-06-29 14:48:48 -07:00 |
|
Sebastian Ullrich
|
9f7af2b77b
|
doc: document a few tactics
|
2021-06-29 06:35:45 -07:00 |
|
Sebastian Ullrich
|
20fa503803
|
fix: move elabCommand parts that should happen only once into new function
|
2021-06-29 06:34:15 -07:00 |
|
Sebastian Ullrich
|
a993e0baa0
|
fix: non-dependent arrow should not extend local context
|
2021-06-29 06:31:37 -07:00 |
|
Leonardo de Moura
|
e5d4af5e75
|
refactor: split Syntax.lean
|
2021-06-28 13:52:04 -07:00 |
|
Leonardo de Moura
|
953dd85c06
|
chore: avoid inline
|
2021-06-28 10:17:01 -07:00 |
|
Leonardo de Moura
|
ae6a28af52
|
chore: remove unnecessary specialize
|
2021-06-28 10:11:23 -07:00 |
|
Leonardo de Moura
|
8f9fa8d04c
|
refactor: add BuiltinTactic.lean
|
2021-06-28 10:08:42 -07:00 |
|
Leonardo de Moura
|
712206f80e
|
refactor: add BindersUtil.lean
|
2021-06-28 08:44:16 -07:00 |
|
Leonardo de Moura
|
7e1bb3e65b
|
refactor: add MatchAltView.lean and PatternVar.lean
|
2021-06-28 08:29:47 -07:00 |
|
Leonardo de Moura
|
7f986c62ba
|
refactor: add Arg.lean
|
2021-06-28 08:10:16 -07:00 |
|
Leonardo de Moura
|
795b15581b
|
refactor: add BuiltinTerm.lean
|
2021-06-28 07:55:52 -07:00 |
|
Sebastian Ullrich
|
fc821745ae
|
fix: swallow exception on hover formatting
|
2021-06-23 23:29:46 +02:00 |
|
Wojciech Nawrocki
|
40f07ef6a1
|
fix: make mangling injective again
|
2021-06-23 00:08:20 -07:00 |
|
Wojciech Nawrocki
|
05d46348c7
|
fix: 32-bit Unicode name mangling
|
2021-06-23 00:08:20 -07:00 |
|
Sebastian Ullrich
|
cef3ade164
|
fix: info on non-atomic simp args
|
2021-06-23 00:08:07 -07:00 |
|
Gabriel Ebner
|
3cff5ceb99
|
perf: make trace[...] ... notation lazy
|
2021-06-23 00:07:27 -07:00 |
|
Gabriel Ebner
|
6a4982622f
|
fix: nontermination in Syntax.reprint
|
2021-06-23 00:07:27 -07:00 |
|
Sebastian Ullrich
|
1c2aacc4a8
|
fix: worker: don't wait for tasks on exit
|
2021-06-23 08:53:20 +02:00 |
|
Sebastian Ullrich
|
0948742da1
|
perf: fix formatting info tree unconditionally
|
2021-06-22 10:22:08 +02:00 |
|
Sebastian Ullrich
|
479edbe235
|
refactor: avoid unnecessary withLCtx
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
30a0954424
|
refactor: revert MonadRef changes
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
65f2874d86
|
chore: address reviews
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
eb1e285e26
|
chore: style
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
b8be90fa08
|
fix: do not show complex terms in hover
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
736d32c026
|
fix: hover on synthetic sorry
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
91e3100e30
|
fix: properly resolve syntax kinds in macro/elab_rules
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
3f4ab0a2af
|
feat: implement elab_rules
TODO: infer category from quotation type
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
a86efc4796
|
fix: info tree context of command macros
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
9101c9d5da
|
feat: support docstrings on syntax/macro/...
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
14ceae0b0b
|
feat: remove hover restriction to first token
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
652097e184
|
fix: separate ElabInfo from MacroExpansionInfo, always emit the former before the latter
This way all hover info is contained in the former info node kinds
|
2021-06-21 10:17:26 -07:00 |
|