search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
170 stars 49 forks source link

RFC: Math in hovers #541

Open Vtec234 opened 1 month ago

Vtec234 commented 1 month ago

Proposal

Now that the hover tooltips in the infoview support displaying math (#534), it would be awesome if tooltips in the editor also did. Implementation-wise, it may be possible to do whatever LaTeX-Workshop does.

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

mhuisi commented 1 month ago

For documentation purposes: LaTeX-Workshop appears to render LaTeX as an SVG and then converts that to a data:image/svg+xml;base64, data URL.