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

Work in progress: alternative hovers #114

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

rhencke
Copy link

@rhencke rhencke commented Jun 21, 2017

This introduces alternate hovers for type info/doc info, trying to extract what is needed from the returned IDE info of :docs-for/:type-of.

This is not complete yet - it's hard to extract and reformat it all correctly.

But, I was hoping to get your feedback on a couple things:

  • Are you interested in this change?
  • Do you have any suggestions in approach?

Thanks for your work!

Previous New
oldhover1 hover1
oldhover2 hover2
(types only) oldtypeonlyhovers (types only) hovertypeonly

@rhencke
Copy link
Author

rhencke commented Jun 21, 2017

I am not sure why the Appveyor one doesn't work, sorry

@zjhmale
Copy link
Owner

zjhmale commented Jul 31, 2017

Hi @rhencke, I think it's just a random glitchy of the CI tool, I re-triggered it and everything is fine 😄

@zjhmale
Copy link
Owner

zjhmale commented Jul 31, 2017

And yeah extract useful and correct information for hover from Idris executable is quite tricky in some scenarios, honestly I like your idea here, just show the most important information for the user.

@zjhmale
Copy link
Owner

zjhmale commented Jul 31, 2017

But, I think it is better to deliver this feature as a configuration like others here https://github.com/zjhmale/vscode-idris/blob/master/package.json#L104

@zjhmale
Copy link
Owner

zjhmale commented Jul 31, 2017

Maybe you are also interested on this #117 😄

@zjhmale
Copy link
Owner

zjhmale commented Jul 31, 2017

And sorry for the huge delay, since I'm quite busy with other things, and get offline for weeks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants