leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
137 stars 25 forks source link

Gray mouse-over documentation boxes problematic on small screens #228

Open TentativeConvert opened 1 month ago

TentativeConvert commented 1 month ago

Here’s an image to illustrate what I mean by “gray mouse-over documentation box”:

image

It can happen that such a gray mouse-over documentation box covers the whole screen, particular on small displays.
(They can be much bigger than what is displayed in the image above. I saw one example of such a box covering the whole display of an ipad, but I cannot now reconstruct what that box documented.)

The only way to make such a box disappear again seems to be to click somewhare outside of the box. But if it covers the whole screen that’s impossible. Even if it covers only part of the screen, it may be impossible to click outside the box without clicking some button you don’t want to click.

So I think we need an easier way to close these boxes, or an upper bound on the percentage of screen area they are allowed to cover.