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

155 commits

Author SHA1 Message Date
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
Daniel Fabian
63d58c2f64 refactor: use Except instead of Option in the JSON code. 2021-06-07 12:10:10 +02:00
Gabriel Ebner
501c31da4d feat: send $/lean/fileProgress notification 2021-06-05 13:49:28 +02:00
Sebastian Ullrich
c5957dc069 fix: ignore other leanpkg print-paths output 2021-05-31 17:39:55 +02:00
Sebastian Ullrich
619873c842 feat: make System.FilePath opaque 2021-05-28 14:19:59 +02:00
Sebastian Ullrich
4354534fda feat: make FilePath a concrete type 
Resolves #363
 2021-05-28 14:19:59 +02:00
Wojciech Nawrocki
18e6f78089
fix: publish header processing message log 2021-05-26 09:30:29 +02:00
Sebastian Ullrich
4d6c178a6a refactor: server: actually detect EOF at goalsAt? 2021-05-21 17:13:33 -07:00
Leonardo de Moura
a3e09a983f chore: remove leftovers 2021-05-17 14:47:04 -07:00
Leonardo de Moura
3b7bcdc449 feat: add endPos field to SourceInfo.original 
We need an update stage0 before we use it.
 2021-05-17 14:32:58 -07:00
Sebastian Ullrich
6a03e15a79 feat: watchdog: show message while worker is starting 2021-05-14 14:59:47 +02:00
Sebastian Ullrich
1e6dadfa52 fix: documentHighlight on partial input 
Fixes #455
 2021-05-11 17:03:18 +02:00
Sebastian Ullrich
8863761401 feat: show initial state for tactic combinators by default 2021-05-02 23:07:15 +02:00
Sebastian Ullrich
e1cde87c43 fix: server: completion & goal state at EOF 2021-04-30 19:25:53 +02:00
Daniel Fabian
0238bf8c33 refactor: use Ordering inside of rbmap instead of lt. 2021-04-27 07:58:58 -07:00
Leonardo de Moura
2667744092 fix: panic message 2021-04-15 18:25:19 -07:00
Sebastian Ullrich
92810602d0 fix: server: do not stop processing after error (except for header error) 2021-04-12 22:41:10 +02:00
Sebastian Ullrich
af588078e0 fix: server: output import errors again 2021-04-09 12:40:38 +02:00
Sebastian Ullrich
cc9577add2 refactor: server: remove SnapshotData 2021-04-08 22:10:27 +02:00
Sebastian Ullrich
dd15c8d5a7 feat: worker: don't abort on import error 
to avoid the "crashed" message
 2021-04-08 22:10:27 +02:00
Sebastian Ullrich
c3d6f781cf refactor: publishDiagnostics 2021-04-08 22:10:27 +02:00