Please review an update to the `jdk-default.css` stylesheet used for specifications and tool guides. The original purpose was to make use of the Dejavu web fonts provided by the API docs and to update the navigation bar to match the one in the API docs. However, the updates include some other fixes and improvements also described below.
- The change to use the DejaVu web fonts consists only of the `@import` statement in line 16 as the stylesheet already used DejaVu web fonts as first choice in its `font-family` rules. - The changes to make the navigation bar match the one in the API docs are mostly located at the end of the file (beyond line 160). However, this also includes setting the `margin` property to '0' in the `body` element and adding a `margin` in the `main` and `footer` elements instead. - To set the horizontal margin for page content elements outside the `main` element which occur in some pages, a margin is set explicitly on those elements in lines 48-50. While this is a bit awkward, I think it's still better than working with negative margins in the header to offset the margin in the `body` element. - Most of the remaining changes (lines 53-110) are changes are to redefine the styles in simpler terms, such as leaving out declarations that are equal to browser defaults, and removing the units from `0`-length values. The changes are intended to preserve the layout of the pages, including the body font size which is slightly different from the one used in API docs (`10pt` vs `14px`). I can provide before/after snapshots of the rendered documentation if desired. ------------- Commit messages: - JDK-8329617: Update stylesheet for specs and tool documentation Changes: https://git.openjdk.org/jdk/pull/18694/files Webrev: https://webrevs.openjdk.org/?repo=jdk&pr=18694&range=00 Issue: https://bugs.openjdk.org/browse/JDK-8329617 Stats: 73 lines in 1 file changed: 27 ins; 19 del; 27 mod Patch: https://git.openjdk.org/jdk/pull/18694.diff Fetch: git fetch https://git.openjdk.org/jdk.git pull/18694/head:pull/18694 PR: https://git.openjdk.org/jdk/pull/18694
