Scott Morrison
007b1b5979
feat: extend API of KVMap ( #2851 )
2023-11-09 22:59:56 +11:00
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
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
Scott Morrison
076908d13b
feat: replay constants into an Environment ( #2617 )
...
* feat: replay constants into an Environment
2023-10-11 14:08:03 +11:00
int-y1
8d7520b36f
chore: fix typos in comments
2023-10-08 10:46:05 +02:00
kuruczgy
83c7c29075
fix: XML parsing bugs ( #2601 )
...
* fix: make XML parser handle trailing whitespace in opening tags
* fix: make XML parser handle comments correctly
---------
Co-authored-by: György Kurucz <me@kuruczgy.com>
2023-10-04 11:51:22 +11:00
Joachim Breitner
b2d668c340
perf: Use flat ByteArrays in Trie ( #2529 )
2023-09-20 13:22:37 +02:00
Scott Morrison
c318d5817d
feat: allow configuring occs in rw
2023-09-13 12:03:18 -07:00
Eric Wieser
1f3ef28a1d
fix: correct universe polymorphism in Lean.instFromJsonProd
...
The previous type was
```
Lean.instFromJsonProd.{u, v} {α β : Type (max u v)} [FromJson α] [FromJson β] :
FromJson (α × β)
```
where universe metavariable assignment assigned the wrong universe to both types!
2023-08-06 07:32:30 -07:00
Siddharth
b9ec36d089
chore: get rid of all inline C annotations for LLVM ( #2363 )
2023-07-30 10:39:40 +02:00
Leonardo de Moura
bebf1927f8
chore: remove workarounds
2023-06-21 20:35:33 -07:00
Sebastian Ullrich
7987b795bb
fix: workspace symbols
...
Somehow was broken by #2233
2023-06-06 14:58:24 +02:00
Mario Carneiro
01ba75661e
fix: implement String.toName using decodeNameLit
...
fixes #2231
2023-05-28 17:38:57 -07:00
Gabriel Ebner
e6b3202df3
chore: remove dead code
2023-03-08 15:54:07 -08:00
Rishikesh Vaishnav
600758ba49
fix: fuzzy-find bonus for matching last characters of pattern and symbol ( #1917 )
2023-01-19 09:06:53 +01:00
Sebastian Ullrich
38bd089a45
feat: introduce custom leanSorryLike semantic token type for sorry, admit, stop
2023-01-04 10:50:02 +01:00
Siddharth
b6eb780144
feat: LLVM backend ( #1837 )
2022-12-30 12:45:30 +01:00
Gabriel Ebner
d19033e443
fix: correctly parse json unicode escapes
2022-12-23 17:04:10 -08:00
Gabriel Ebner
14f8ff1642
feat: add CoeOut class
2022-12-21 04:24:39 +01:00
Gabriel Ebner
118567657d
chore: remove dangerous instances in json-rpc
2022-12-21 04:24:39 +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
Mario Carneiro
17ef0cea8a
feat: intra-line withPosition formatting
2022-11-28 09:02:08 -08:00
Scott Morrison
a3dfa5516d
feat: add HashSet.insertMany
2022-11-28 06:59:21 -08:00
Sebastian Ullrich
7529e86307
feat: implement workspace/applyEdit server request ( #1846 )
2022-11-17 19:30:17 +00:00
Sebastian Ullrich
36189cb51a
chore: simplify parser cache key computation, panic on environment/token table divergence
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
da6efe1bca
fix: make parser caching sound (I hope?)
2022-11-11 09:13:02 +01:00
Mario Carneiro
4fefb2097f
feat: hover/go-to-def/refs for options
2022-11-07 20:01:13 +01:00
Leonardo de Moura
25beba6624
feat: avoid modulo in HashMap and HashSet
...
closes #609
Context: trying to improve Lean startup time.
Remark: it didn't seem to make a difference in practice. We should
investigate more.
cc @kha @gebener
2022-10-27 18:54:56 -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
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
Leonardo de Moura
3505b60a22
feat: probing helper functions
2022-10-15 08:51:20 -07:00
Rishikesh Vaishnav
76c4693c95
fix: improve fuzzy-matching heuristics ( #1710 )
2022-10-14 16:17:14 +02:00
Leonardo de Moura
767bda2c28
chore: preparing to change the semantics of @[inline] instance
...
In the new code generator, we are going to lambda lift the instance
methods before saving the code at the end of the base phase. The goal is to make instance
ligth weight and cheap to inline. The anotation `@[inline]` is going
to be an annotation for the lambda lifted methods.
2022-10-11 20:35:56 -07:00
Gabriel Ebner
ba57ad3480
feat: add implementation-detail hypotheses
2022-10-11 17:24:35 -07:00
Chris Lovett
3eeb064d83
fix: Clear Diagnostics when file is closed ( #1591 )
2022-10-07 17:28:15 -07:00
Sebastian Ullrich
5b7e6661f9
chore: more RBMap cleanup
2022-10-06 17:26:43 -07:00
Leonardo de Moura
e9d5dfc689
chore: closes #1683
2022-10-04 16:46:08 -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
12deab6516
feat: RBMap simplifications
2022-10-03 17:08:55 -07:00
Ed Ayers
22bb798995
feat: datatypes for LSP code actions ( #1654 )
2022-09-28 09:07:39 +00:00
Mario Carneiro
85119ba9d1
chore: move Std.* data structures to Lean.*
2022-09-26 05:46:04 -07:00
Mario Carneiro
97bcc7fd7c
feat: add ForM -> ForIn adapter
2022-09-25 06:40:56 -07:00
Leonardo de Moura
e51b078015
fix: incorrect annotations
2022-09-24 14:20:21 -07:00
Sebastian Ullrich
3288f437c2
refactor: further simplify RBMap balancing
2022-09-24 14:16:48 +02:00
