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

Fix hover #133

Open
michaelmesser opened this issue Dec 29, 2021 · 1 comment
Open

Fix hover #133

michaelmesser opened this issue Dec 29, 2021 · 1 comment
Labels
bug Something isn't working feature: hover

Comments

@michaelmesser
Copy link
Contributor

michaelmesser commented Dec 29, 2021

Hover sometimes doesn't return the correct value.

f : Bool -> Bool
f = \case
    True => False
    False => True
          *  ^

If a save, then hover over ^ I get Prelude.True : Bool. However, if I hover over * then hover over ^, I get Test.case block in f : Bool -> Bool. Is this caused by overlapping ranges being added to the cache?

Also, for a better user experience hover should return a range.

I tried to fix this at one point but ran into idris-lang/Idris2#1506 and idris-lang/Idris2#1543

Additionally hover should show documentation. There also is probably a better way to handle hiding/showing implicit arguments.

@michaelmesser michaelmesser added bug Something isn't working feature: hover labels Dec 29, 2021
@michaelmesser michaelmesser pinned this issue Jan 17, 2022
@ianmelendez95
Copy link

If anyone else is having an issue with this, I've found a quick way to 'reset' is to just edit the line (I add a space and remove it), save the file again, and then move up and down to get it to reload the arguments.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working feature: hover
Projects
None yet
Development

No branches or pull requests

2 participants