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

660 commits

Author SHA1 Message Date
mhuisi
b5348786a6 fix: pre-dependency-build-mode compatibility 2023-10-13 16:42:19 +02:00
mhuisi
253a5b931d fix: correct handling of FileWorker restarts 2023-10-13 16:42:19 +02:00
mhuisi
9945fa04d6 feat: FileWorker handling of --no-build 2023-10-13 16:42:19 +02:00
Sebastian Ullrich
4e1d95ce58 feat: pass along extra print-paths flags and handle no-build Lake error in server 2023-10-13 16:42:19 +02:00
Sebastian Ullrich
a2e2481c51 feat: cancel tasks on document edit 2023-10-13 09:52:26 +02:00
int-y1
8d7520b36f chore: fix typos in comments 2023-10-08 10:46:05 +02:00
Mario Carneiro
e6fe3bee71 fix: hover term/tactic confusion 2023-09-26 10:16:37 +02:00
thorimur
018020d36f
fix: uninterpolated error message in registerRpcProcedure (#2547) 2023-09-18 11:39:04 +02:00
tydeu
926663505e chore: split up & simplify importModules 2023-08-31 15:37:33 -04: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
Sebastian Ullrich
aeb60764c1 feat: auto-complete declaration names in arbitrary namespaces 2023-07-28 07:50:09 -07:00
Sebastian Ullrich
687f50ab33 fix: never show private names in completion 2023-07-28 07:50:09 -07:00
Sebastian Ullrich
c268d7e97b fix: kill descendant processes on worker exit 2023-07-05 23:42:53 +02:00
Wojciech Nawrocki
ba4bfe26f2 fix: add missing instantiateMVars 2023-06-27 16:13:56 -07:00
Mario Carneiro
2348fb37d3 fix: use Lean.initializing instead of IO.initializing 2023-06-17 06:57:14 -07:00
Sebastian Ullrich
8d4dd2311c fix: increase semantic token highlight limit 2023-05-21 10:17:35 +02:00
Mario Carneiro
ad4b822734 fix: use snake case for @[code_action_provider] 2023-05-08 22:25:48 +02:00
Sebastian Ullrich
a4f732e6b1 fix: ignore vanishing files during watchdog update 2023-03-10 19:13:24 +01:00
Sebastian Ullrich
aacab14394 chore: remove support for text-mode I/O 
This didn't do anything except on Windows, where it would make the
application differ from standard Windows applications, which we don't
want.
 2023-03-10 16:27:56 +01:00
Sebastian Ullrich
f24608c4d1 fix: make eoi an actual command with info tree 2023-01-26 13:05:57 +01: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
Wojciech Nawrocki
184ca3ddb0 chore: bump server version 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
Gabriel Ebner
eeab2af7ae fix: remove Inhabited Environment instance 2022-12-21 20:08:08 +01:00
Gabriel Ebner
443c1a08e5 fix: lsp change debouncing 2022-12-21 20:02:53 +01:00
Sebastian Ullrich
88c8cd5cf2 fix: show correct goal state after an empty by 2022-12-13 01:39:45 +01:00
Gabriel Ebner
4b87103931 chore: ignore document version errors 2022-12-03 01:20:47 +01:00
Sebastian Ullrich
bc0684a29c fix: work around VS Code completion bug 2022-11-29 19:14:45 +01:00
Sebastian Ullrich
a38bc0e6ed refactor: revise server architecture 
Replace complex debouncing logic in watchdog with single `IO.sleep` in
worker `didChange` handler, replace redundant header change logic in
watchdog with special exit code from worker.
 2022-11-29 00:52:24 +01:00
Sebastian Ullrich
7529e86307
feat: implement workspace/applyEdit server request (#1846) 2022-11-17 19:30:17 +00:00
Mario Carneiro
4fefb2097f feat: hover/go-to-def/refs for options 2022-11-07 20:01:13 +01:00
Sebastian Ullrich
f39281f6b4 fix: hoverableInfoAt? in presence of canonical syntax 2022-10-25 12:23:13 +02:00
Gabriel Ebner
041307fd4b fix: build 2022-10-20 12:42:32 -07:00
E.W.Ayers
46112a5f2a fix: review 2022-10-20 11:20:42 -07:00
E.W.Ayers
c9a26596dc refactor: switch resolve to double eval strategy 
Using option (2) from this comment:
https://github.com/leanprover/lean4/pull/1661#pullrequestreview-1135363727
 2022-10-20 11:20:42 -07:00
E.W.Ayers
691835037e feat: code action resolvers 2022-10-20 11:20:42 -07:00
E.W.Ayers
297d06fc0c fix: issue where code action was not running 2022-10-20 11:20:42 -07:00
E.W.Ayers
c795e2b073 fix: rm CodeActionData 2022-10-20 11:20:42 -07:00
Ed Ayers
7f47a34656 style: apply suggestions from code review 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
 2022-10-20 11:20:42 -07:00
E.W.Ayers
260e42b0a7 doc: fix docs from review 2022-10-20 11:20:42 -07:00
E.W.Ayers
8085ce88e9 feat: CodeActionProvider 
This is a low-level system for registering LSP code actions.
Developers can register their own code actions.
In future commits I am going to add features on top of this.
 2022-10-20 11:20:42 -07:00
Mario Carneiro
583e023314 chore: snake-case attributes (part 2) 2022-10-19 09:28:08 -07:00
Mario Carneiro
dd5948d641 chore: snake-case attributes (part 1) 2022-10-19 09:28:08 -07:00
Gabriel Ebner
fb4d90a58b feat: dynamic quotations for categories 2022-10-18 14:59:14 -07:00
Mario Carneiro
c06cffa54f refactor: rename isExitCommand -> isTerminalCommand 2022-10-12 11:11:31 -07:00
Mario Carneiro
8dfae9eb38 feat: import command stub 2022-10-12 11:11:31 -07:00
Gabriel Ebner
ba57ad3480 feat: add implementation-detail hypotheses 2022-10-11 17:24:35 -07:00