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

446 commits

Author SHA1 Message Date
Leonardo de Moura
d5f1a5d1d1 fix: in-word completion 
closes #857
 2021-12-10 15:48:35 -08:00
Sebastian Ullrich
a4633d30e2 fix: option completion after trailing . 2021-12-10 14:19:19 -08:00
Sebastian Ullrich
ce2e733f17 fix: make option completion work in presence of value 2021-12-10 14:19:19 -08:00
Leonardo de Moura
47c2d335d4 fix: completion for aliases 
closes #863
 2021-12-10 12:14:11 -08:00
Joscha
e4406f1785 fix: find references to function parameters in function body 
With #861, the server can now connect the occurrences of parameters in the
function definition and in the function body to each other.
 2021-12-10 15:25:43 +01:00
Joscha
12ee541622 fix: reference fields in constructor correctly 2021-12-10 15:25:43 +01:00
Joscha
11ba6dc216 test: add simple "find references" test 2021-12-10 15:25:43 +01:00
Sebastian Ullrich
a329896e70 feat: refine declaration ranges at instance & example 2021-11-27 07:25:15 -08:00
Sebastian Ullrich
4f15805787 feat: annotate declarations with term infos 2021-11-27 07:25:15 -08:00
larsk21
e641ae4eae fix: prefix check in set_option completion 2021-11-26 11:42:54 +01:00
Sebastian Ullrich
f7decd2d46 fix: go to definition for macro_rules etc. 2021-11-24 11:54:13 +01:00
larsk21
9028405798 fix: handle _root_ in unresolveNameGlobal with pp.fullNames 2021-11-21 15:23:21 +01:00
larsk21
8cf520209f feat: show fully-qualified name in hover text 2021-11-21 15:23:21 +01:00
Leonardo de Moura
5f119cb54f feat: avoid metavariables at CompletionItems 
Not sure whether it helps or creates more confusion.
Note that we are still using the `?` prefix for metavariables on the
InfoView and hover info.
 2021-10-29 08:01:21 -07:00
Leonardo de Moura
68120b24b8 feat: add docstring to CompletionItem 
closes #746
 2021-10-28 08:14:40 -07:00
Daniel Selsam
b36baa143f feat: improved name-unresolving in delab 
Fixes #641
 2021-09-07 16:26:00 +02:00
Wojciech Nawrocki
feff4c2ed3 feat: unify goal handlers 2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
e8af38f586 chore: fix tests 2021-08-24 08:57:41 -07:00
Sebastian Ullrich
20accf5105 feat: revise macro parameter syntax 2021-08-12 07:48:42 -07:00
Leonardo de Moura
1d9d8c7e75 chore: fix tests 
close #402
 2021-08-07 13:22:58 -07:00
Daniel Selsam
e6b90dde8f fix: pp.analyze mvars can bottom-up 2021-08-03 09:13:18 +02:00
Daniel Selsam
c3d62c1076 chore: patch tests for pp.analyze default 2021-08-03 09:13:18 +02:00
Leonardo de Moura
635bc78d72 feat: use structure extension to implement Structure.lean 2021-08-02 18:03:20 -07:00
Sebastian Ullrich
42e681a5a6 fix: make unterminated comments consume all input 
Fixes #549
 2021-07-22 15:55:12 +02:00
Sebastian Ullrich
7e317d23db feat: term info on where declarations 2021-07-19 13:24:59 -07:00
Sebastian Ullrich
b76dd1a8e3 feat: go-to-definition for local variables 2021-07-19 13:24:59 -07:00
Sebastian Ullrich
df57b43b06 fix: go-to-type on parameterized types 2021-07-19 13:24:59 -07:00
Sebastian Ullrich
18becc7d7d fix: plain term goal on binders 2021-07-19 13:24:59 -07:00
Sebastian Ullrich
4a4b4c1ef4 fix: mkAtomFrom: generate synthetic position like other *From functions 
Also consistently use binders as reference position for an elided binder type.
Before, type errors were always given extent 1, the length of the
synthetic `_` token.
 2021-07-19 13:24:59 -07:00
Wojciech Nawrocki
7aca461a35 fix: hovers on elabFieldName fields 2021-07-19 09:55:37 +02:00
Wojciech Nawrocki
bcde967d99 feat: add dot hover test 2021-07-19 09:55:37 +02:00
Wojciech Nawrocki
e89aa5641e chore: auto-insert newlines 2021-07-05 19:42:01 +02:00
Wojciech Nawrocki
49e6f42a6b chore: remove absolute paths from test 2021-07-05 19:42:01 +02:00
Wojciech Nawrocki
fd9e3d8fe6 chore: add completion test and go-to field type 2021-07-05 19:42:01 +02:00
Leonardo de Moura
818efe719e fix: fixes #533 2021-06-29 15:20:46 -07:00
Sebastian Ullrich
fc821745ae fix: swallow exception on hover formatting 2021-06-23 23:29:46 +02:00
Sebastian Ullrich
cef3ade164 fix: info on non-atomic simp args 2021-06-23 00:08:07 -07:00
Sebastian Ullrich
d5810d5c6f chore: disable LSAN in server tests for now 2021-06-23 08:53:20 +02:00
Sebastian Ullrich
b8be90fa08 fix: do not show complex terms in hover 2021-06-21 10:17:26 -07:00
Sebastian Ullrich
736d32c026 fix: hover on synthetic sorry 2021-06-21 10:17:26 -07:00
Sebastian Ullrich
9170d1ff99 test: some syntax docstring tests 2021-06-21 10:17:26 -07:00
Sebastian Ullrich
da4c46370d feat: store elaborator declaration name in info tree 2021-06-21 10:17:26 -07: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
Gabriel Ebner
501c31da4d feat: send $/lean/fileProgress notification 2021-06-05 13:49:28 +02:00
Sebastian Ullrich
93327e2324 fix: tactic state on {/· 2021-05-21 17:13:33 -07:00
Sebastian Ullrich
9f3ddb0c43 fix: do not store solved goals in info tree 2021-05-20 15:17:54 -07:00
Sebastian Ullrich
a02c6fd3eb chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
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
a2cafbf56f test: for tactic state visualization bug 2021-05-17 15:12:50 -07:00