## Stream: general

### Topic: tooltips on keywords

#### Johan Commelin (Apr 21 2020 at 06:56):

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 (Apr 24 2020 at 12:39):

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

#### Gabriel Ebner (Apr 24 2020 at 12:42):

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 (Apr 24 2020 at 13:48):

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...

Last updated: May 06 2021 at 22:13 UTC