Go-to-definition for types in hover

[larsk21]

@Kha suggested exploring how go to definition could look like for a type shown in a hover. It seems the front end part of this feature would work quite well, with a few drawbacks.

1. Markdown code blocks ( ```lean) do not support links, so we would need to switch to language independent HTML code blocks (<code>) for the type in the hover (not for the documentation with possible lean code examples).
2. This would require enabling HTML in hovers in the client (with a limited set of allowed tags for security reasons), which is currently only support per MarkdownString, i.e. needs to be set for each incoming hover text. This is supposed to change with LSP 3.17 (see this issue).
3. Although this works in VSCode and other Markdown renderers, I'm not sure if links (of the form []()) are always rendered as such inside HTML code blocks, which might be relevant for other editors or if a renderer is changed.
4. HTML code blocks do not fill the hover completely and have a slightly darker background, which looks a bit weird.

The benefit, of course, is the possibility of jumping to the definition of a type appearing in the type of an expression in the code, which I find quite useful. What do you all think of it?

[Kha]

We might eventually want to upgrade the hover to a full info view, of course, but I don't think this is quite as important here and would require much more work in both client and server.

[Vtec234]

Btw, I am planning to add go-to-def for hovers in the infoview, but insofar as we are using the default LSP hover infrastructure here, it would be an orthogonal feature.

[gebner]

This would require enabling HTML in hovers in the client

More importantly, it also requires the client to support the HTML we use in the hovers. So the server needs to detect whether the editor supports it, and fall back to the current output otherwise. Apparently not even vscode supports it yet if I read the issue correctly, and even once it does only a limited (and unspecified) subset of HTML will be supported. I don't expect emacs and neovim to quickly support the same subset either.

I'm not sure if links (of the form ) are always rendered

A related question is whether links are opened in the editor or in the web browser. It's obviously much less useful if they're opened in the browser.

We might eventually want to upgrade the hover to a full info view, of course, but I don't think this is quite as important here and would require much more work in both client and server.

My preferred solution would be to add an RPC call that simply returns the information in the hover (i.e., name, type, documentation, the expression itself (?), etc.). This is not particularly hard to implement on the server side (it should be easier than emitting correct HTML), and is what we eventually want anyhow, as you point out. On the client side, it depends on the editor. In the neovim plugin, adding support for hovers via RPC would be trivial (we already have hover commands for interactive diagnostics, goals, etc.). The vscode extension would require a bit of refactoring though, because the RPC code is completely tied to the infoview at the moment.

[Vtec234]

My preferred solution would be to add an RPC call that simply returns the information in the hover (i.e., name, type, documentation, the expression itself (?), etc.).

Note that we already have Lean.Widget.InteractiveDiagnostics.infoToInteractive. But it's undocumented and the types are bit messy. I am hoping to submit a PR soon which cleans this API up and makes it usable from user widgets.