search

meraymond2 / idris-vscode

Idris front-end for VS Code
MIT License
59 stars 10 forks source link

Feature request: Jump to definition, Ctrl-Click. #76

Open Kiiyya opened 2 years ago

Kiiyya commented 2 years ago

It would be super handy to be able to ctrl-click go-to-definition on any identifier, if possible also on operators (since notation in idris2 is very frightening for beginners like me). The hover already works and is useful, but often I am interested in what else is contained in a given module. At least for me, go-to-definition is my Nr 1 feature in any language IDE extension. I'm using idris2.

Thanks for making this extension :)

michaelmesser commented 2 years ago

Go to definition is supported by idris2-lsp-vscode. However, installing the LSP can be a bit tricky.

meraymond2 commented 2 years ago

Hi, thanks for making an issue.

I'm not aware of any simple way to implement this. This extension is mostly a wrapper around Idris’s IDE protocol, and I don't think it exposes the information I would need. I'll have a think though.

In the meantime, you could try the lsp extension michaelmesser recommended. The language server has some functionality that the IDE protocol doesn't, although the last time I looked it still had some missing features. I'm not sure how easy it is to run the two extensions side-by-side — I need to investigate that and update the readme.

michaelmesser commented 2 years ago

I don't think it would be a good idea to run the extensions side by side. I will have some time over the next month to work on improving the LSP so let me know what is missing.

doofin commented 1 year ago

@meraymond2 Would it be a good idea to implement this in idris2 compiler and add a new command in language protocols?