-
Notifications
You must be signed in to change notification settings - Fork 95
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
Remove bold settings from dark theme CSS #763
base: master
Are you sure you want to change the base?
Conversation
@vogella Could you take a look? The issue is that some preferences are being specified in the css file and if the user changes them, they get reset by the css file. I changed it so only colors are specified, but don't use dark theme so can't say if the change causes any issue for end-users. |
@jjohnstn sorry I recently had to switch laptops for repair and have no development setup for JDT and therefore cannot test. If the dark theme still looks like for a new Java file in a new workspace, I think the change is OK. |
Ok, thanks @vogella The real change is all the additional bells and whistles that aren't enabled by default. The old CSS turned almost all of them on. Any enablement settings current users have shouldn't be altered by updating to the change. A brand new workspace just doesn't have the optional things enabled by default (such as additional colors for enum or abstract classes) but they are easily settable and the settings are preserved/stored across sessions. I'll check it in for M1 and see if anybody has issues. |
I've removed M1 milestone, that is long overdue. Feel free to set any reasonable milestone instead. |
ping @vogella |
Jeff, what is the status of this one? |
@akurtakov I initially had a change which simply removed the bold settings from the dark theme CSS and then I also removed some more non-color settings, but it changes the behavior when a user switches to dark mode the first time since some bold settings are not set by default so I wasn't sure this was going to go over with end-users. I was hoping to eventually see if settings could be or were already separated for the themes. It makes sense that the settings should be for a theme and not global. I just never got around to it. |
What it does
Removes bold settings from dark theme CSS so user can set them.
How to test
See issue.
Author checklist