Feature request: Jump to definition, Ctrl-Click.

[Kiiyya]

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]

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

[meraymond2]

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]

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]

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