RFR: JDK-8292594: Use CSS custom properties for all fonts and colors

[Hannes Wallnöfer]

Please review a patch to complete the conversion of the javadoc style sheet to use CSS custom properties for all colors and fonts. 

A few notes for changes that may not be self-explanatory:

 - I renamed the `--highlight` property prefix used for the active navigation/menu/tab item to `--selected` as the term "highlight" is used for other things such as snippet highlights and active search item targets.
 - I unified the active color of  copy-to-clipboard buttons to one single value even though they appear on different backgrounds. The value works reasonably well for all uses, and can be changed with a single custom property.
 - The stylesheet contains a rule for green line numbers in source pages created with the `-linksource` option. This is a very rarely used option so I chose to use a custom property with no defined value but a default value. This means the custom property is not contained in the list of custom property definitions in the style sheet, but it can be defined by a theme if needed.
 - I removed CSS selectors that are either illegal under HTML 5 such as a[name] or unused.
 
This change does not affect the appearance of the generated documentation in the browser. I can provide before/after output including different themes if needed.

-------------

Commit messages:
 - Fix indentation
 - JDK-8292594: Use CSS custom properties for all fonts and colors

Changes: https://git.openjdk.org/jdk/pull/11109/files
 Webrev: https://webrevs.openjdk.org/?repo=jdk&pr=11109&range=00
  Issue: https://bugs.openjdk.org/browse/JDK-8292594
  Stats: 83 lines in 2 files changed: 23 ins; 27 del; 33 mod
  Patch: https://git.openjdk.org/jdk/pull/11109.diff
  Fetch: git fetch https://git.openjdk.org/jdk pull/11109/head:pull/11109

PR: https://git.openjdk.org/jdk/pull/11109