Integrated: 8329617: Update stylesheet for specs and tool documentation

[Hannes Wallnöfer]

On Tue, 9 Apr 2024 13:06:28 GMT, Hannes Wallnöfer <hannesw at openjdk.org> wrote:

> 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.

This pull request has now been integrated.

Changeset: 4eb1eaf0
Author:    Hannes Wallnöfer <hannesw at openjdk.org>
URL:       https://git.openjdk.org/jdk/commit/4eb1eaf04477b9a8947a57655cf36380b5b88b5c
Stats:     73 lines in 1 file changed: 27 ins; 19 del; 27 mod

8329617: Update stylesheet for specs and tool documentation

Reviewed-by: jjg

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

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