Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Upgrade frontend to work with Aya language server #21

Merged
merged 7 commits into from
Jun 12, 2022
Merged

Upgrade frontend to work with Aya language server #21

merged 7 commits into from
Jun 12, 2022

Conversation

imkiva
Copy link
Member

@imkiva imkiva commented Jun 12, 2022

Changes:

@imkiva imkiva added the enhancement New feature or request label Jun 12, 2022
@ice1000
Copy link
Member

ice1000 commented Jun 12, 2022

I see, nice!

@ice1000
Copy link
Member

ice1000 commented Jun 12, 2022

bors r+

@bors
Copy link
Contributor

bors bot commented Jun 12, 2022

Build succeeded:

@bors bors bot merged commit 6c3fdfd into main Jun 12, 2022
@bors bors bot deleted the refactor branch June 12, 2022 17:40
bors bot added a commit to aya-prover/aya-dev that referenced this pull request Jun 12, 2022
424: New features to LSP r=ice1000 a=imkiva

this PR upgraded LSP4j to 0.14 with inlay hints support; added some features to the LSP backend:
- Inlay type hints for bind patterns (feel free to suggest more)
- CodeLens of each definition showing `%d usages`
- Code folding for definitions that occupy 3 or more LOC.
- Search Everywhere in VSCode (symbols only since VSC does not ask more from backend)

Try it: https://github.com/aya-prover/aya-vscode/suites/6895435995/artifacts/267446633

## See also
Language Server Protocol has recently upgraded to 3.17, and VSCode stabilized their inlay hints APIs
- https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_inlayHint
- rust-lang/rust-analyzer#11445
- microsoft/vscode-languageserver-node#495
- aya-prover/aya-vscode#21


Co-authored-by: imkiva <imkiva@islovely.icu>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants