Zulip Chat Archive

Stream: general

Topic: tooltips on keywords


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip 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