Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC