leanprover/verso

toggle displaying information

Opened this issue · 1 comments

It would be nice to display information such as the type of variable on mouse-over, but I think it could be annoying.
I suggest that it should be possible to switch it on and off.

I imagine that there is a fa-eye (font-awesome) button in the code block which, if pressed, would prevent the information from being displayed.

This is a nice idea!