This was added to control percentage sizes, in
79956b96e8
Now, the only percentage size is [`border-radius`], which is
based on the size of the box itself, not its containing block.
This leaves the property unused.
[`border-radius`]: https://developer.mozilla.org/en-US/docs/Web/CSS/border-radius
This is very dependent on subjectivity and what screen you use,
but this change makes the radio buttons' outer circle less ugly.
This is because I could see the pixels very clearly, thanks to the
very thin line and high contrast. This change makes both less
severe, giving your browser's antialiasing algorithm more to
work with. Since it's thicker, lowering the contrast shouldn't
impact visibility.
* Changes the class names so that they all start with `setting-`.
That should make it harder to accidentally use a setting class outside
the settings popover, where loading the CSS might accidentally change
the styles of something unrelated.
* Get rid of an unnecessary wrapper DIV around the radio button line.
* Simplify CSS selectors by making the DOM easier and more intuitive
to target.
These rules were copied from normalize.css 3, and are mostly redundant.
* `optgroup` isn't used in rustdoc at all
* `textarea` is only used for the "copy" button, so it's not visible
* The remaining buttons and inputs mostly have styles set anyway.
* We should never be setting `color` without also setting the
background to something. Otherwise, you get white-on-gray
text. That seems to be [the reason] why `normalize.css` changed this.
[the reason]: https://github.com/necolas/normalize.css/pull/502
Previously, the radio button choices for themes would wrap awkwardly on
narrow screens. With this change, the group of choices will prefer
bumping down to the next line together, leaving the setting name on its
own line.
Also fix some minor spacing issues:
- Align the setting name vertically with the radio button choices.
- Use margin instead of padding for most spacing choices.
- Use no margin/padding on the right-hand side.
This reduces the number of clicks required to change theme.
Also, simplify the UI a bit (remove setting grouping), and add a "Back"
link close to the settings icon.
