Sebastian Ullrich
cd5dbc66ce
fix: isolate std streams for all commands in server mode
...
Fixes #475
2021-05-19 13:30:54 +02: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
8ae726203d
fix: plainGoal: consider original positions only when deciding whether a tactic is a combinator
2021-05-12 10:51:42 +02:00
Sebastian Ullrich
1e6dadfa52
fix: documentHighlight on partial input
...
Fixes #455
2021-05-11 17:03:18 +02:00
Sebastian Ullrich
84d3896ea7
chore: fix comment
2021-05-05 15:08:30 +02:00
Sebastian Ullrich
4fb01f7c06
fix: goal state on ;
2021-05-03 13:32:00 +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
e6e12ca408
fix: fixes #408
2021-04-22 19:07:03 -07:00
Leonardo de Moura
1dca9d18d4
fix: missing tactic state info on broken proofs
2021-04-18 20:13:02 -07:00
Sebastian Ullrich
e96a21631b
refactor: move elaboration error filtering into Elab.Command
...
Also make it dependent on presence of `missing` instead of parse error,
which means that messages from complete commands that are immediately followed
by parse errors are not filtered out anymore
2021-04-17 23:44:57 +02:00
Leonardo de Moura
2667744092
fix: panic message
2021-04-15 18:25:19 -07:00
Sebastian Ullrich
435431ca7e
feat: hide elaboration errors from partial syntax trees by default
2021-04-13 19:24:35 +02:00
Leonardo de Moura
40a42128be
fix: auto completion improvements
2021-04-12 19:22:56 -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
Leonardo de Moura
3318c75bed
fix: make sure borrow annotations do not affect auto-completion
2021-04-09 13:47:28 -07:00
Sebastian Ullrich
af588078e0
fix: server: output import errors again
2021-04-09 12:40:38 +02:00
Leonardo de Moura
a1887df4ee
feat: include parent structures and aliases in dot notation auto completion
2021-04-08 19:22:31 -07: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
Sebastian Ullrich
bba8184d3b
feat: server: treat import errors as fatal
2021-04-08 22:10:27 +02:00
Sebastian Ullrich
a027b34d58
chore: remove dubious server-only option
2021-04-08 22:10:27 +02:00
Leonardo de Moura
a0a4b9faec
fix: filter declarations that are not valid dot methods
2021-04-08 11:48:12 -07:00
Sebastian Ullrich
f75ce86f71
fix: server: go to type definition
2021-04-08 18:54:53 +02:00
Sebastian Ullrich
d75d7aa0d5
fix: server: ignore unknown implementation-dependent notifications
...
Fixes #383
2021-04-08 09:54:36 +02:00
Sebastian Ullrich
5b5a882da6
fix: watchdog: do not reorder messages while delaying edits
2021-04-07 17:12:37 +02:00
Sebastian Ullrich
43fcf69485
fix: watchdog: mark request as pending even if worker crashed
2021-04-07 16:48:12 +02:00
Leonardo de Moura
803161d9fc
fix: propagate expected type
2021-04-05 20:00:05 -07:00
Leonardo de Moura
3ccd992dad
feat: elaborate auxiliary completion node
2021-04-05 19:07:39 -07:00
Leonardo de Moura
d6af843683
chore: remove completion auxiliary parser
2021-04-05 11:26:13 -07:00
Leonardo de Moura
19fcd518bf
chore: fix syntax
2021-04-05 07:16:59 -07:00
Leonardo de Moura
ba3dd181f5
fix: make sure type errors do not break server
...
We often try to auto-complete code containing errors.
So, the methods `inferType` and `isDefEq` used during completion may
throw exceptions.
2021-04-04 20:29:20 -07:00
Leonardo de Moura
e8cf38de20
feat: improve auto completion matching
2021-04-04 20:03:13 -07:00
Leonardo de Moura
fb67b49719
fix: missing completion
2021-04-04 18:32:56 -07:00
Leonardo de Moura
820495ce7a
feat: black list auxiliary match applications
2021-04-04 10:37:13 -07:00
Leonardo de Moura
0586fe3200
feat: activate auto completion
...
There are many pending TODO's, and issues with the error recovery code.
We also need a test suite.
2021-04-03 21:01:17 -07:00
Leonardo de Moura
09ee8bddad
feat: tactic name completion
2021-04-03 15:45:44 -07:00
Leonardo de Moura
20f569c033
feat: set_option completion
2021-04-03 15:06:50 -07:00
Leonardo de Moura
0a94aaabc9
feat: use expected type to prioritize completion candidates
2021-04-03 14:12:42 -07:00
Leonardo de Moura
398bbcfce3
feat: save aditional information for id completion, and suppress implicit prefix when reporting completion types
2021-04-03 12:53:32 -07:00
Leonardo de Moura
ff1d27370c
feat: add CompletionInfo
2021-04-02 20:44:57 -07:00
Leonardo de Moura
d26aa5e1ab
feat: black list other auxiliary constructions
2021-04-02 16:21:54 -07:00
Sebastian Ullrich
e20b2c359a
feat: server: show goal state after tactic if cursor not strictly before tactic
2021-04-03 00:23:46 +02:00
Leonardo de Moura
ed4504929d
refactor: add Server/Completion.lean
...
Add environment extension for black listing declaritions for completion.
2021-04-02 11:10:06 -07:00
Leonardo de Moura
9815d626f5
feat: hide auxiliary constructions when generating completion candidates
2021-04-02 11:10:06 -07:00
Leonardo de Moura
bc44ad65ae
feat: only consider dot completion info occurring in the hover line
2021-04-02 11:10:06 -07:00
