tooltips on keywords

Stream: general

[Johan Commelin]

What would it take to enable tooltips on keywords? Then we could explain the difference between def and lemma or between structure and class right where it matters. I think this would be helpful for new users.

[Patrick Massot]

I think this is entirely from the Lean C++ side. VScode will display anything sent by the Lean server

[Gabriel Ebner]

I see two options here:

1. As Patrick proposed, implement this on the server side. This should be one call to info_manager from structure_cmd/definition_cmd.
2. Implement this in the vscode extension. We already have two HoverProviders that produce tooltips: one for the error messages, and one for type \lambda. You could add a third one that looks at the word at the requested position and returns an interesting tooltip if the word is "lemma" or "structure".

[Johan Commelin]

Option (1) seems the best. So let me vote for that. It doesn't seem to be difficult, but I wouldn't know where to start...