larsk21
dcbc526115
feat: report header processing errors as error progress
2021-12-15 13:00:05 +01:00
Gabriel Ebner
45bcef5dab
refactor: server: use String.firstDiffPos to find changes
...
This is necessary so that we do not reprocess the whole file if
incremental sync is disabled.
2021-12-14 11:55:34 -08:00
Sebastian Ullrich
c6c56b15e1
feat: findSysroot? & reworked initSearchPath
2021-11-20 11:04:39 +01:00
Sebastian Ullrich
8df2b07209
refactor: remove double exception layer in RequestM
2021-11-09 16:58:13 +01:00
Sebastian Ullrich
138d9eea43
fix: server: custom search path should win over package one should win over system one
...
I think that's all permutations now
2021-11-09 14:27:13 +01:00
Sebastian Ullrich
e92f7f1b4b
refactor: server: assume 1 info tree per snapshot
2021-11-04 18:31:36 +01:00
Wojciech Nawrocki
128a71c726
fix: excessive RPC logging
2021-11-01 09:11:31 -07:00
Sebastian Ullrich
f202c7c322
fix: prefer local search path
2021-10-22 12:48:37 +02:00
Sebastian Ullrich
91f1948f50
fix: Lake search path
2021-10-22 12:30:30 +02:00
Sebastian Ullrich
b3c8ee2923
fix: add Lake to built-in search path
2021-10-19 10:57:13 +02:00
Sebastian Ullrich
6a90b30875
fix: prefer user-given search paths
2021-10-19 10:57:13 +02:00
Sebastian Ullrich
08dbf239a6
chore: server: redundant let
2021-10-15 06:56:02 -07:00
Sebastian Ullrich
674e473c84
feat: server: support LAKE env var
2021-10-15 06:56:02 -07:00
Sebastian Ullrich
6a1897302b
chore: server: use exit code to communicate absence of package
2021-10-15 06:56:02 -07:00
Sebastian Ullrich
765ed37409
feat: server: support Lake
2021-10-15 06:56:02 -07:00
Sebastian Ullrich
0a43a9c466
refactor: use JSON to communicate between server & package manager
2021-10-08 11:28:04 +02:00
Sebastian Ullrich
3787c6081c
fix: pass worker cmdline options to Lean code
2021-09-08 11:34:31 +02:00
Wojciech Nawrocki
2f5fbf3b13
feat: support multiple RPC sessions
...
Motivation: we may want to also use RPC in editor insets, or multiple
webviews in general.
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
1b68daef39
fix: clear messages earlier
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
c948d87a28
chore: forgot import
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
f7e9ba76dd
perf: cache diagnostics in server
...
Reason 1: we were making quadratically many pretty-printer calls since each `publishMessages` would format the entire `MessageLog`.
Reason 2: we want to avoid formatting each diagnostic twice, once as interactive, and once as plain LSP diagnostic.
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
cc23a21d3e
chore: cleanup
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
72df64e8fe
chore: move RpcSession
2021-08-24 08:57:41 -07:00
Daniel Selsam
6940166db4
chore: rebase and rm rawPos
2021-08-03 09:13:18 +02:00
Daniel Selsam
89364b802b
feat: top-down heuristic delaboration
2021-08-03 09:13:18 +02:00
Wojciech Nawrocki
1d57ffb4d7
refactor: shuffle classes to avoid dependency loops
2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
1311f87a8b
feat: eagerly initialize RPC session
...
With this we are able to send RpcRefs immediately, in particular in (interactive) diagnostics.
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
Wojciech Nawrocki
f27a069773
chore: drop UntypedRef and use monotonic RpcRefs
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
ffc6efd5d0
fix: use properly random RPC session id
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
9a5cdaf506
chore: address review 1
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
4a93c9ac1c
chore: purify WorkerM
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
f891279957
chore: drop one namespace
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
Sebastian Ullrich
0839ead35e
perf: server: avoid redundant publishDiagnostics
...
This should reduce server & editor load for the common case where most
command do *not* emit diagnostics
2021-07-08 12:12:19 +02:00
Wojciech Nawrocki
c7beb283e9
feat: allow requests to log to stderr
2021-07-05 19:42:01 +02:00
Sebastian Ullrich
1c2aacc4a8
fix: worker: don't wait for tasks on exit
2021-06-23 08:53:20 +02:00
Sebastian Ullrich
eb1e285e26
chore: style
2021-06-21 10:17:26 -07:00
Wojciech Nawrocki
bd4af2b340
feat: routing of custom LSP requests
2021-06-15 22:53:19 +02:00
Wojciech Nawrocki
4b3987c9cb
feat: LSP request handler registration
2021-06-15 22:53:19 +02:00
Wojciech Nawrocki
39931566a0
feat: separate RequestContext in server
2021-06-15 22:53:19 +02:00
Gabriel Ebner
f5f9be191b
fix: show expected type in term goal
2021-06-07 16:23:22 -07:00
Gabriel Ebner
5786f58738
feat: plain term goal request
2021-06-07 16:23:22 -07:00
