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

New features to LSP #424

Merged
merged 16 commits into from
Jun 12, 2022
Merged

New features to LSP #424

merged 16 commits into from
Jun 12, 2022

Conversation

imkiva
Copy link
Member

@imkiva imkiva commented Jun 12, 2022

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

@imkiva imkiva added the lsp label Jun 12, 2022
@imkiva imkiva added this to the v0.19 milestone Jun 12, 2022
@codecov
Copy link

codecov bot commented Jun 12, 2022

Codecov Report

Merging #424 (a5d765f) into main (1db9c22) will decrease coverage by 0.00%.
The diff coverage is 92.18%.

@@             Coverage Diff              @@
##               main     #424      +/-   ##
============================================
- Coverage     81.73%   81.72%   -0.01%     
  Complexity     2492     2492              
============================================
  Files           230      230              
  Lines          7677     7679       +2     
  Branches        943      943              
============================================
+ Hits           6275     6276       +1     
- Misses          929      930       +1     
  Partials        473      473              
Impacted Files Coverage Δ
base/src/main/java/org/aya/concrete/Expr.java 92.59% <ø> (ø)
base/src/main/java/org/aya/concrete/Pattern.java 100.00% <ø> (ø)
base/src/main/java/org/aya/concrete/TacNode.java 0.00% <ø> (ø)
...src/main/java/org/aya/concrete/stmt/BindBlock.java 100.00% <ø> (ø)
...e/src/main/java/org/aya/concrete/stmt/Command.java 82.35% <ø> (ø)
...c/main/java/org/aya/concrete/stmt/GenericDecl.java 100.00% <ø> (ø)
...rc/main/java/org/aya/concrete/stmt/Signatured.java 81.81% <0.00%> (-8.19%) ⬇️
base/src/main/java/org/aya/concrete/stmt/Stmt.java 94.44% <ø> (ø)
base/src/main/java/org/aya/core/Matching.java 100.00% <ø> (ø)
base/src/main/java/org/aya/core/def/ClassDef.java 0.00% <ø> (ø)
... and 38 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 6695e1f...a5d765f. Read the comment docs.

Copy link
Member

@ice1000 ice1000 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors r+

(LensMaker lmfao)

@bors
Copy link
Contributor

bors bot commented Jun 12, 2022

Build succeeded:

@bors bors bot merged commit f4d52bd into main Jun 12, 2022
@bors bors bot deleted the lsp branch June 12, 2022 19:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants