Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
248 stars 25 forks source link

Infoview tooltips should render their contents as markdown #329

Open Julian opened 7 months ago

Julian commented 7 months ago

The built-in LSP hover handler properly renders hover popups as markdown, e.g.:

Screenshot 2024-01-14 at 10 07 13 AM

But our custom popups in the infoview (for tooltips) do not, see e.g.:

Screenshot 2024-01-14 at 10 07 58 AM

Julian commented 6 months ago

See the output from #help command for a particularly egregious example, as it's a full document.