Joscha
bfc185e98e
fix: don't duplicate definition and declaration requests
2022-01-31 21:36:37 +01:00
Joscha
4545e183d8
fix: go to definition in modified file
2022-01-31 21:36:37 +01:00
Joscha
ccf492b61d
feat: implement partial ilean updates
2022-01-31 21:36:37 +01:00
Wojciech Nawrocki
2d1cea0864
feat: inform server if widgets are available
2022-01-29 10:04:25 +01:00
Leonardo de Moura
cf3b8d4eb4
chore: cleanup
...
Make the code style more uniform.
We still have a lot of leftovers from the old frontend.
2022-01-26 09:18:17 -08:00
Sebastian Ullrich
cfaba85199
feat: load precompiled modules in the server
2022-01-25 23:25:52 +01:00
Leonardo de Moura
2192e6148b
chore: remove coe, coeSort, and coeFun abbreviations
...
The notation `↑ e` is now expanded eagerly.
See #403
2022-01-20 15:19:06 -08:00
Joscha
2423a78db4
refactor: implement suggestions
2022-01-20 17:20:01 +01:00
Sebastian Ullrich
3a926b1047
fix: use user-facing private decl name in symbol query
2022-01-20 17:20:01 +01:00
Sebastian Ullrich
53d90a71ae
feat: do case-sensitive symbol query if query contains upper-case char
2022-01-20 17:20:01 +01:00
Sebastian Ullrich
1168334cca
fix: Unicode symbol lookup
2022-01-20 17:20:01 +01:00
Joscha
7540889bd3
feat: implement LSP workspace symbol request
2022-01-20 17:20:01 +01:00
Joscha
3651ebb377
fix: don't send worker notification to client
2022-01-19 16:29:10 +01:00
Sebastian Ullrich
3abb70dbb5
refactor: factor out common source search path logic
2022-01-18 18:22:50 +01:00
Leonardo de Moura
be4c86f780
chore: remove temporary workarounds
2022-01-17 17:03:15 -08:00
Leonardo de Moura
f8653a8cb7
chore: add temporary workaround
2022-01-17 16:58:39 -08:00
Leonardo de Moura
dd3d8f6fad
feat: complete namespaces
...
closes #940
2022-01-17 10:03:36 -08:00
Leonardo de Moura
b970919978
chore: remove unnecessary Inhabited
2022-01-14 19:48:10 -08:00
larsk21
b712918db9
fix: unify handleDefinition for imports
2022-01-14 10:32:06 +01:00
larsk21
ecaa004dcc
feat: make withWaitFindSnap consider all snaps of a document
2022-01-14 10:32:06 +01:00
larsk21
e584560b17
feat: enable "go to definition" for imports
2022-01-14 10:32:06 +01:00
larsk21
89bbaf514e
feat: include imports in header snap info tree
2022-01-14 10:32:06 +01:00
Sebastian Ullrich
d503fe6d13
refactor: avoid double exception layer with AsyncList
2022-01-14 09:18:57 +01:00
Joscha
d8ec900ae9
refactor: use array instead of list in AsyncElabState
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
b9f8f5eb38
fix: find references of function parameters
2022-01-14 09:18:57 +01:00
Joscha
281ede6ed4
feat: handle references notifications
2022-01-14 09:18:57 +01:00
Joscha
f98cf0289c
feat: send references notification when file evaluation finishes
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
088433dc57
refactor: let AsyncList creation be stateful
2022-01-14 09:18:57 +01:00
Joscha
67aa823ae2
fix: resolve symlinks for the LSP client
2022-01-14 09:18:57 +01:00
Joscha
bce56fdc0c
feat: implement reference request
2022-01-14 09:18:57 +01:00
Joscha
7abdf94fc5
feat: respond to reference request in watchdog
2022-01-14 09:18:57 +01:00
Joscha
4fd1d22c31
feat: load and unload ileans on LSP notifications
2022-01-14 09:18:57 +01:00
Joscha
4e12cc902b
feat: load ilean files from olean search path
2022-01-14 09:18:57 +01:00
Joscha
567a854a15
feat: load search path for source files in watchdog
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
Joscha
3f998c68bc
feat: export reference info to ilean files
2022-01-14 09:18:57 +01:00
Joscha
96ed620933
feat: collect reference info from InfoTrees
2022-01-14 09:18:57 +01:00
Joscha
efb964956e
feat: add FileRefMap and convert to/from JSON
2022-01-14 09:18:57 +01:00
Gabriel Ebner
dc65bb080a
fix: race condition in RPC request handler
2022-01-10 13:37:40 +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
Gabriel Ebner
83e167dfb5
feat: append filename to worker command-line
...
This change has no effect on the server behavior. The only difference
is that the filename now shows up in `htop`, `ps`, etc., which makes it much
easier to see what Lean processes are running, and which are using 100%
CPU, etc.
2022-01-04 15:10:46 +01:00
Mac
748c9ab73a
chore: tweak error message
...
Co-authored-by: Wojciech Nawrocki <wjnawrocki+gh@protonmail.com>
2021-12-27 09:44:11 +01:00
tydeu
30bdd4e751
doc: add docstring for chainLspRequestHandler
2021-12-27 09:44:11 +01:00
tydeu
004e172f5d
feat: LSP request handler chaining
2021-12-27 09:44:11 +01:00
Sebastian Ullrich
51dc32957b
feat: show universe args on hover
...
We might also want to replace them with fresh vars to make the hover
completely independent of the context, but this change at least avoids
any hidden information.
2021-12-20 10:51:44 +01:00
Sebastian Ullrich
5f96a9fc4d
fix: do not show type of sort in hover
...
Fixes #896
2021-12-19 11:03:15 +01:00
