search

expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
https://expln.github.io/lamp/latest/index.html
MIT License
13 stars 5 forks source link

Proposal (low priority): Make tooltips work on smartphones (in addition to larger displays) #23

Open david-a-wheeler opened 1 year ago

david-a-wheeler commented 1 year ago

Background: I've experimented using metamath-lamp on my smartphone. It was surprisingly good!! Reasoning backwards took longer, but it's still useful. However, because touchscreen devices (like smartphones) don't have "hover", users of touchscreens can't see the tooltips. The lack of tooltips really hurts discoverability on the smartphone, which is too bad since otherwise the experience is generally pretty good.

So I think the code should be tweaked so that tooltips show on "regular" computers and on smartphones. For example, the tooltip should show on a long downpress (smartphone) or hover. A down+up (click) should activate whatever it is.

Here's some information on how to configure tooltips like this:

https://stackoverflow.com/questions/69030402/material-ui-tooltip-is-not-working-on-mobile

This isn't the only issue on smartphone, as I don't know of a way to distinguish left-button from Alt+left-button. That might need to be fixed separately.. but making tooltips work should at least be easy :-).

expln commented 1 year ago

Despite this issue is of a low priority, I feel like you consider supporting mobile devices quite an important part of mm-lamp (taking into account other issues and propositions). Initially I didn't have plans to support mobile devices just because I don't have enough time. But I may reconsider this (however, this will not add time for me :) ) Why do you think mobile devices are so important to support for this tool?

david-a-wheeler commented 1 year ago

Several reasons.

Supporting phones means you can do this anywhere "on the go". Many people have access only to their phone much of the time. Also, many people only have access to a mobile phone.

Finally, as a "gateway drug" phone access is awesome. It really lowers the barrier to entry.. people can start trying things out immediately.

Currently the big limit is that you can't change the statement type (H or P, and maybe someday G). If thar limit were removed (say with a new icon that toggled the statement type) then the phone has feature parity.

david-a-wheeler commented 1 year ago

I don't think this is necessary for version 11, but at some future point it'd be great for smartphone users to be able to see the tooltips, and hover doesn't work on touch screens. Here's one approach:

Maybe tooltips could be revealed on "touch-down" and disappear on "touch-up" (but not on mousedown & mouseup, since hover works if you can do that)? If you can move off the item before touch-up, then users can see the tooltip without being forced to complete a tap or long-tap. Then the GUI would be far more discoverable on a smartphone.

david-a-wheeler commented 1 year ago

It appears that MUI tooltips can be confired to use "Hover or touch" instead of just "hover". The touch delay should probably be set to whatever the long-press value is. Then you get tooltips on smartphones:

https://mui.com/material-ui/react-tooltip/