leanprover
Notation tooltips in the infoview
When a user hovers over notation in the infoview we should be able to pop up a tooltip with the info about how to type that character. See Zulip discussion.
Tooltips for declarations / names in the infoview seem like they would be much harder.
Tooltips for declarations / names in the infoview seem like they would be much harder.
We could try to extend the support we have in place for the documentation generation introduced by https://github.com/leanprover-community/lean/pull/89 Right now, it only includes the full constant name (for every name, notation, {, ⟨, etc. that occurs in the expression). Extending it to also output filename and position shouldn't be too hard. We could even enable it by default if we start the server with -Dpp.links_with_pos=true.
