max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
32663 commits 1 branch 0 tags 5.3 GiB
Commit graph

25 commits

Author SHA1 Message Date
Marc Huisinga
3c82f9ae12
feat: diagnostics for stale dependencies (#3247) 
Sends a diagnostic informing the user to run Restart File when a file
dependency is saved.

Based on #3014 because this feature was easier to implement with the new
architecture.

ToDo:
- [x] Adjust vscode-lean4 to display a notification when this diagnostic
appears in a non-annoying way
(https://github.com/leanprover/vscode-lean4/pull/393)
- [x] Use a file watcher to identify changes to files not tracked by VS
Code
- [x] Rebase onto master when #3014 is merged
 2024-03-18 10:38:38 +00:00
Henrik Böving
23e49eb519 perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Ed Ayers
22bb798995
feat: datatypes for LSP code actions (#1654) 2022-09-28 09:07:39 +00:00
Jonathan Coates
04e60cebd1 feat: LSP code folding support 
The following constructs are foldable:
 - Sections and namespaces
 - Blocks of import/open statements
 - Multi-line commands (so mostly definitions)
 - Mutual definitions
 - Module-level doc comments
 - Top-level definition doc comments

Fixes #1012
 2022-03-07 17:23:35 +01:00
Joscha
2823cbc87b feat: implement single-file "find references" in LSP server 2021-12-10 15:25:43 +01:00
Wojciech Nawrocki
ce7f31a654 feat: keep-alive semantics for RPC sessions 2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
55ffb73bbe refactor: rename rpc/initialize to rpc/connect 2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
9a5cdaf506 chore: address review 1 2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
f077dd05d3 feat: RPC ref decrement 2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
4d83e79121 feat: more RPC handlers 2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
3ec568c110 feat: initial RPC 2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
bd4af2b340 feat: routing of custom LSP requests 2021-06-15 22:53:19 +02:00
Gabriel Ebner
5786f58738 feat: plain term goal request 2021-06-07 16:23:22 -07:00
Sebastian Ullrich
63b96f62e7 feat: server: auto completion skeleton 2021-04-01 18:26:17 +02:00
Sebastian Ullrich
ddff87f7f5 feat: server: also implement full semantic token requests 
because lsp-mode freaks out without them
 2021-03-16 16:41:32 -07:00
Sebastian Ullrich
5df753f338 feat: server: support ranged semantic tokens (keywords only for now) 2021-03-16 16:41:32 -07:00
Sebastian Ullrich
e2a8ee8520 feat: highlight corresponding do (if any) when hovering over return 2021-02-26 14:58:09 +01:00
Wojciech Nawrocki
ec903f58d2 feat: bare-bones goal request handler 2021-02-06 10:41:14 +01:00
Wojciech Nawrocki
d9c6a992b5 feat: specify version in waitForDiagnostics 2021-01-22 18:02:31 +01:00
Wojciech Nawrocki
40698ecc07 feat: LSP scaffolding for go-to-definition 2021-01-19 13:22:13 -08:00
Sebastian Ullrich
4c3b247dee feat: server: report document symbol hierarchy 2020-12-31 15:00:59 +01:00
mhuisi
377c3dc6fe feat: add WatchdogM wrapper for testing, collectDiagnostics and remove waitForRequests again after reconsideration 2020-12-23 20:00:36 +01:00
mhuisi
23371c5f82 feat: waitForDiagnostics & waitForResponses requests 2020-12-23 20:00:36 +01:00
Marc Huisinga
37a49afd7b fix: snapshot list divergence & stale diagnostics 2020-12-23 20:00:36 +01:00
Wojciech Nawrocki
e0d2af1805 chore: move to new frontend 2020-12-23 20:00:36 +01:00