Buster Copley
bccbefdc1c
fix: version numbers in code actions ( #2721 )
...
Co-authored-by: Richard Copley <buster@buster.me.uk>
2023-10-24 22:55:47 +11:00
Mario Carneiro
e6fe3bee71
fix: hover term/tactic confusion
2023-09-26 10:16:37 +02:00
Sebastian Ullrich
2eaa400b8e
fix: do not unnecessarily wait on additional snapshot in server request handlers ( #2370 )
...
Co-authored-by: Wojciech Nawrocki <wjnawrocki+gh@protonmail.com>
2023-07-30 05:58:46 +00:00
Wojciech Nawrocki
ba4bfe26f2
fix: add missing instantiateMVars
2023-06-27 16:13:56 -07:00
Sebastian Ullrich
8d4dd2311c
fix: increase semantic token highlight limit
2023-05-21 10:17:35 +02:00
Rishikesh Vaishnav
561e404fe4
feat: make go-to-definition on a typeclass projection application go to the instance(s) ( #1767 )
2023-01-19 09:10:01 +00:00
Wojciech Nawrocki
f5531c2a11
feat: add context and term data to goals
2023-01-13 17:13:02 -08:00
Sebastian Ullrich
fa4cbd93ee
feat: highlight #exit as leanSorryLike
2023-01-04 10:50:02 +01:00
Sebastian Ullrich
38bd089a45
feat: introduce custom leanSorryLike semantic token type for sorry, admit, stop
2023-01-04 10:50:02 +01:00
Sebastian Ullrich
b6bd2dea35
feat: signature pretty printer for hovers
2022-12-21 21:59:05 +01:00
Sebastian Ullrich
bc0684a29c
fix: work around VS Code completion bug
2022-11-29 19:14:45 +01:00
Mario Carneiro
4fefb2097f
feat: hover/go-to-def/refs for options
2022-11-07 20:01:13 +01:00
Gabriel Ebner
ba57ad3480
feat: add implementation-detail hypotheses
2022-10-11 17:24:35 -07:00
Mario Carneiro
d56708c0e5
fix: handle multi namespace/section in foldingRange and documentSymbol ( #1680 )
2022-10-04 17:37:52 +00:00
Mario Carneiro
280d8c9c9b
feat: add (canonical := true) option in Syntax
2022-09-27 22:09:54 +02:00
Ed Ayers
2a6697e077
feat: goal-diffs ( #1610 )
2022-09-24 11:46:11 +02:00
Gabriel Ebner
4246d98547
fix: remove unnecessary BaseIO in AsyncList
2022-09-01 16:57:03 +02:00
Sebastian Ullrich
a657a638f0
feat: sub-info tree level hover
2022-08-31 17:49:43 -07:00
Gabriel Ebner
c7e45722a3
feat: trace nodes with messages
2022-08-15 08:55:25 -07:00
Gabriel Ebner
e9545a426f
refactor: RpcEncodable
2022-08-10 06:31:46 -07:00
Leonardo de Moura
642cf0bc6d
feat: add option pp.showLetValues
...
closes #1345
2022-07-26 17:53:34 -07:00
Sebastian Ullrich
5160cb7b0f
refactor: remove some unnecessary antiquotation kind annotations
2022-07-23 17:09:32 +02:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
Sebastian Ullrich
a10a5335ba
fix: do not highlight module docstrings
...
Fixes #1353
2022-07-22 13:47:47 +02:00
Sebastian Ullrich
1611cf63c3
fix: make document symbols request deterministic
2022-07-19 12:23:03 +02:00
Gabriel Ebner
a8cab84735
refactor: use computed fields for Expr
2022-07-11 14:19:41 -07:00
Leonardo de Moura
e4b358a01e
refactor: prepare to elaborate a[i] notation using typeclasses
2022-07-09 15:24:22 -07:00
Leonardo de Moura
2446c64a99
chore: cleanup
2022-07-04 07:15:04 -07:00
Leonardo de Moura
e8935d996b
chore: String.get?, String.getOp?, and remove String.getOp
2022-07-02 09:59:04 -07:00
Sebastian Ullrich
ae683af9c2
refactor: merge AsyncList.updateFinishedPrefix/finishedPrefix
...
We only ever use both of them together, and forgetting to call the first
one first could lead to subtle bugs.
2022-06-29 17:08:15 +02:00
Sebastian Ullrich
80217cfa90
fix: asynchronous head snapshot fallout
2022-06-28 16:54:29 -07:00
Sebastian Ullrich
86cd656fc6
refactor: adapt raw syntax manipulations to TSyntax
...
Sometimes there's just no structure to work on
2022-06-27 22:37:02 +02:00
Sebastian Ullrich
8979ed42a4
refactor: file worker: wait on header task before dispatching requests
2022-06-24 19:02:00 +02:00
Sebastian Ullrich
e14b4ab0e4
feat: file worker: make header snapshot asynchronous
2022-06-24 19:02:00 +02:00
E.W.Ayers
2edf02544e
chore: rm ExprWithCtx
...
We will make this a separate PR
2022-06-13 16:32:01 -07:00
E.W.Ayers
367bde3601
chore: revert "refactor: replace InfoWithCtx with ExprWithCtx"
...
This reverts commit db342793d53c986b8794084196552c33711f9091.
2022-06-13 16:32:01 -07:00
E.W.Ayers
f64cb95eca
refactor: replace InfoWithCtx with ExprWithCtx
...
This is potentially controversial. There are still some [todo]s that need sorting.
2022-06-13 16:32:01 -07:00
E.W.Ayers
3d561a3ab0
doc: add docstrings for interactive
2022-06-13 16:32:01 -07:00
E.W.Ayers
e3d2080232
refactor: PPExprTaggedRequest -> PPExprTaggedParams
2022-06-13 16:32:01 -07:00
E.W.Ayers
fd66e70d1e
fix: explicit structure for PPExprTaggedRequest
2022-06-13 16:32:01 -07:00
Wojciech Nawrocki
351be06a21
feat: ppExprTagged RPC call
2022-06-13 16:32:01 -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
larsk21
b556e73657
refactor: extend Lsp.ModuleRefs in Server.References
2022-06-03 13:03:52 +02:00
Leonardo de Moura
484e510221
feat: do not use pp.inaccessibleNames = true at getInteractiveTermGoal
...
See discussion at https://github.com/leanprover/vscode-lean4/issues/76
We also use `pp.inaccessibleNames = false` in error messages. In this
setting, an inaccessible name is displayed in the context only if the
target type depends on it.
2022-06-02 16:22:43 -07:00
Wojciech Nawrocki
115c564b18
feat: go to head constant in applications
...
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
cd47c30e47
chore: review fixes
2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
8c67afae2f
feat: generalize getGoToLocation RPC
2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
aef8d32d0b
feat: add RPC call to retrieve defn/decl/type defn
2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
9c058a5798
chore: remove some unnecessary partial
2022-05-31 00:07:56 +02:00
