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
lemma or between
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:
- As Patrick proposed, implement this on the server side. This should be one call to
- 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