Leonardo de Moura
|
9d05023325
|
chore: remove some [specialize] annotations
|
2022-01-18 09:24:06 -08:00 |
|
Sebastian Ullrich
|
37f5be1b26
|
chore: fix servertest_init_exit
|
2022-01-14 09:18:57 +01:00 |
|
Joscha
|
ab52480b69
|
fix: implement suggestions
|
2022-01-14 09:18:57 +01:00 |
|
Joscha
|
4bcf7ab31f
|
style: add copyright headers
|
2022-01-14 09:18:57 +01:00 |
|
Joscha
|
7cce91acb4
|
refactor: move some reference-related types to Lean.Data
These types are required for worker->watchdog notifications.
|
2022-01-14 09:18:57 +01:00 |
|
Joscha
|
bce56fdc0c
|
feat: implement reference request
|
2022-01-14 09:18:57 +01:00 |
|
Joscha
|
87b8afff6b
|
feat: register file watcher for .ilean files
|
2022-01-14 09:18:57 +01:00 |
|
Gabriel Ebner
|
f146d456ce
|
fix: only enable InsertReplaceEdit if supported
|
2022-01-07 20:28:10 +01:00 |
|
larsk21
|
8c2d7a35d3
|
fix: make set_option completion replace typed partial name
|
2022-01-07 17:06:26 +01:00 |
|
Leonardo de Moura
|
de29657594
|
feat: implement bool operator==(data_value const & a, data_value const & b) using Lean autogenerated code
|
2021-12-16 16:37:47 -08:00 |
|
Leonardo de Moura
|
867134614b
|
feat: add constructor DataValue.ofSyntax
|
2021-12-16 15:41:29 -08:00 |
|
Leonardo de Moura
|
7d7c6d8be5
|
feat: add CompletionItemKind
|
2021-12-15 11:24:11 -08:00 |
|
Leonardo de Moura
|
043e9c80b4
|
feat: add Trie.findPrefix
|
2021-12-15 11:24:11 -08:00 |
|
larsk21
|
d50c08360d
|
feat: change error flag to progress kind in LeanFileProgressProcessingInfo
|
2021-12-15 13:00:05 +01:00 |
|
larsk21
|
925c530673
|
feat: add error field to LeanFileProgressProcessingInfo
|
2021-12-15 13:00:05 +01:00 |
|
Leonardo de Moura
|
68bd55af32
|
chore: fix codebase
|
2021-12-10 13:12:09 -08:00 |
|
Joscha
|
e4406f1785
|
fix: find references to function parameters in function body
With #861, the server can now connect the occurrences of parameters in the
function definition and in the function body to each other.
|
2021-12-10 15:25:43 +01:00 |
|
Joscha
|
2823cbc87b
|
feat: implement single-file "find references" in LSP server
|
2021-12-10 15:25:43 +01:00 |
|
Sebastian Ullrich
|
2a1aee2b7a
|
feat: record declaration ranges of builtin parsers & elaborators
|
2021-11-26 17:13:19 +01:00 |
|
Gabriel Ebner
|
d6ba8e597a
|
feat: add range parameter to getInteractiveDiagnostics
|
2021-10-11 22:59:47 +02:00 |
|
Sebastian Ullrich
|
0a43a9c466
|
refactor: use JSON to communicate between server & package manager
|
2021-10-08 11:28:04 +02:00 |
|
Leonardo de Moura
|
fe7b750bce
|
fix: fixes #679
|
2021-09-18 15:34:29 -07:00 |
|
Leonardo de Moura
|
633dc9829e
|
feat: add withOptions
|
2021-09-17 14:20:28 -07:00 |
|
Leonardo de Moura
|
cbe5241663
|
chore: cleanup
|
2021-09-14 19:20:32 -07:00 |
|
Leonardo de Moura
|
db583550fd
|
feat: add Lean.Rat for implementing decision procedures
|
2021-09-14 19:18:12 -07:00 |
|
Leonardo de Moura
|
3714cf16ec
|
refactor: lazy evaluation for <|>
see #617
|
2021-09-07 17:06:10 -07:00 |
|
Leonardo de Moura
|
6f075e6ece
|
feat: add enum command for declaring enumeration types
closes #654
|
2021-09-05 16:58:49 -07:00 |
|
Wojciech Nawrocki
|
198be2c8a7
|
chore: no backticks in Name JSON
|
2021-08-24 08:57:41 -07:00 |
|
Wojciech Nawrocki
|
e4fb367f20
|
chore: make rpc/connect a request
|
2021-08-24 08:57:41 -07:00 |
|
Wojciech Nawrocki
|
fd016c6065
|
chore: address some comments
|
2021-08-24 08:57:41 -07:00 |
|
Wojciech Nawrocki
|
568cc3cf11
|
refactor: consistent naming of widget modules
|
2021-08-24 08:57:41 -07:00 |
|
Wojciech Nawrocki
|
ce7f31a654
|
feat: keep-alive semantics for RPC sessions
|
2021-08-24 08:57:41 -07:00 |
|
Wojciech Nawrocki
|
d116e2e923
|
feat: batch RPC release
|
2021-08-24 08:57:41 -07:00 |
|
Wojciech Nawrocki
|
ae24d8a2db
|
feat: interactive diagnostics take 1
|
2021-08-24 08:57:41 -07:00 |
|
Wojciech Nawrocki
|
d7c3866e14
|
perf: tail-recursive Json.compress
|
2021-08-24 08:57:41 -07:00 |
|
Wojciech Nawrocki
|
2a20d41cd9
|
feat: BEq Json
|
2021-08-24 08:57:41 -07:00 |
|
Wojciech Nawrocki
|
dae1a94d53
|
feat: misc server additions
|
2021-08-24 08:57:41 -07:00 |
|
Leonardo de Moura
|
6ced2cdece
|
refactor: move lean_name_eq to runtime, add lean_name_hash in C
|
2021-08-16 16:13:55 -07:00 |
|
Leonardo de Moura
|
4b58c4cc02
|
refactor: instances that "hide" coercions
Example:
```
instance [CoeHTCT α β] [Add β] : HAdd α β β where
hAdd a b := Add.add a b
```
|
2021-08-13 17:18:55 -07:00 |
|
Leonardo de Moura
|
2dfde4637f
|
fix: index out of bounds
|
2021-08-12 05:39:19 -07:00 |
|
Leonardo de Moura
|
c913886938
|
chore: add private annotations
|
2021-08-03 18:15:39 -07:00 |
|
Leonardo de Moura
|
01d902f905
|
feat: add register_option command
User-defined options.
|
2021-08-03 14:31:04 -07:00 |
|
Leonardo de Moura
|
526cbfbcd0
|
refactor: add ImportingFlag.lean
|
2021-08-03 14:29:36 -07:00 |
|
Wojciech Nawrocki
|
f1b4d9a193
|
chore: restore non-generic Format
Motivation: it is unclear whether this is the best solution for embedding objects in pretty-printer outputs.
|
2021-08-01 09:58:44 +02:00 |
|
Wojciech Nawrocki
|
f51b80060d
|
feat: generic tagged Format
|
2021-08-01 09:58:44 +02:00 |
|
Wojciech Nawrocki
|
d3ca1e98e9
|
refactor: make lsp/release a notification
|
2021-08-01 09:58:44 +02:00 |
|
Wojciech Nawrocki
|
55ffb73bbe
|
refactor: rename rpc/initialize to rpc/connect
|
2021-08-01 09:58:44 +02:00 |
|
Leonardo de Moura
|
6cc30a3f90
|
feat: add NameSSet
Staged set of names
|
2021-07-31 14:24:00 -07:00 |
|
Leonardo de Moura
|
2abafd9df4
|
feat: add "staged set" helper type
|
2021-07-31 14:23:29 -07:00 |
|
Leonardo de Moura
|
bd60e59f9a
|
feat: add HashMap.insert'
The new function returns a flag indicating whether the new entry
replaced an existing or not.
We use it to implement `importModules`.
|
2021-07-31 13:42:01 -07:00 |
|