Leonardo de Moura
68120b24b8
feat: add docstring to CompletionItem
...
closes #746
2021-10-28 08:14:40 -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
Wojciech Nawrocki
e843fb7ca5
fix: widget messages
2021-10-17 10:01:23 +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
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
Wojciech Nawrocki
07f99eba73
fix: use local context from Info node in widgets
2021-10-04 21:09:44 +02:00
Leonardo de Moura
6a880fecc9
chore: modify findDocString?
2021-09-21 17:29:40 -07:00
Chris Lovett
d32b4ffb24
fix: make sure logs folder exists
2021-09-16 09:46:10 +02:00
Leonardo de Moura
42436254ee
fix: code
2021-09-12 19:11:21 -07:00
Sebastian Ullrich
3787c6081c
fix: pass worker cmdline options to Lean code
2021-09-08 11:34:31 +02:00
Wojciech Nawrocki
b6971e4733
fix: don't crash watchdog on notifications to closed files
2021-09-04 18:50:27 -07:00
Leonardo de Moura
391366ef24
refactor: add annotation for displaying conv state
2021-09-02 15:52:11 -07:00
Leonardo de Moura
1a362bc212
feat: add support for displaying conv goal in interactive mode
2021-09-01 16:45:12 -07:00
Wojciech Nawrocki
0dea880aba
doc: diagnostic diff in snapshots
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
1076d3ed2f
chore: bump server version
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
0897984a95
feat: send expression range in interactive term goal
2021-08-24 08:57:41 -07: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
03dbfaea03
chore: remove ExprWithCtx
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
916e80a906
fix: optional type for plain goal 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
feff4c2ed3
feat: unify goal handlers
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
f52940160e
feat: better interactive goals
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
c316a8ea69
fix: syntax not updating in header snapshots
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
8207ca6493
feat: more widget Info integration
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
7ecea27986
feat: emit MessageData from Infos
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
Wojciech Nawrocki
dae1a94d53
feat: misc server additions
2021-08-24 08:57:41 -07:00
Leonardo de Moura
1be41f2adb
chore: fix stdlib
2021-08-06 12:58:58 -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
Leonardo de Moura
cfb7e27b87
fix: isStructure vs isStructureLike
2021-08-02 18:54:19 -07:00
Wojciech Nawrocki
5f021baa95
style: statement ordering
...
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
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
d2e23ff5cf
fix: deriving RpcEncoding
2021-08-01 09:58:44 +02:00
