open_locale docstrings

Stream: general

[Johan Commelin]

Can we turn (for example) https://github.com/leanprover-community/mathlib/pull/2932/files#diff-5fc70a6c00d9ce52e2b06b9c5762d692R136
into a docstring that will show up when you hover of the "classical" in open_locale classical?

[Johan Commelin]

In general it would also be nice if you could hover over open_locale nat and get a pop-up window that shows which commands are executed.