Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: add a setting to disable the loading spinner animation #561

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

YnirPaz
Copy link

@YnirPaz YnirPaz commented Dec 22, 2024

The loading spinner animation in the infoview can be distracting. This PR adds a setting, disabled by default, that removes the animation.

@Vtec234
Copy link
Member

Vtec234 commented Jan 12, 2025

You seem to have a different opinion than #470 :) IMO adding a new option for this rather specific preference is too much maintenance burden. However, the infoview CSS can be tweaked using the 'Lean 4 > Infoview: Style' option, so you should already be able to make the spinner invisible. But it might be a bit hard because it has no specific classes; so how about this: have the PR add a 'loading-spinner' which does nothing to className. Then you can easily make elements with that class invisible in 'Infoview: Style'.

@YnirPaz
Copy link
Author

YnirPaz commented Jan 12, 2025

You seem to have a different opinion than #470 :) IMO adding a new option for this rather specific preference is too much maintenance burden. However, the infoview CSS can be tweaked using the 'Lean 4 > Infoview: Style' option, so you should already be able to make the spinner invisible. But it might be a bit hard because it has no specific classes; so how about this: have the PR add a 'loading-spinner' which does nothing to className. Then you can easily make elements with that class invisible in 'Infoview: Style'.

Alright, I'll do this. But I will say I really don't like having an accessibility "feature" only available for people who have the know-how to code it. I had to make my own version of the extension without the spinner just to be able to use lean comfortably, and it's been frustrating to say the least.

Hopefully this doesn't come off as oversensitive.

@Vtec234
Copy link
Member

Vtec234 commented Jan 13, 2025

I didn't realize this was an accessibility issue rather than just personal preference - that certainly changes things. Owing to very limited dev resources, the accessibility story isn't great (see e.g. #54), but I don't see why not start fixing it here.

I still think just disabling the spinner sounds overly specific, though, and a more general accessibility option would be better. If it is okay to ask here, would it help you if the spinner icon did still appear, but didn't move (i.e., a static icon would show up)? If so, there could be an 'Accessibility > Reduce Motion' option which should set the CSS featutre prefers-reduced-motion. If this would not suffice, do you happen to know if there is another general accessibility option that completely disabling the spinner (i.e., not having it show up at all) could fall under?

Finally, it might be that the current maintainers (CC @mhuisi) are happy with the PR as-is, in which case I certainly wouldn't oppose it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants