Skip to content
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.

Sign up for GitHub

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

Jump to bottom

CSS adjustments in post-processed HTML manual #10497

Merged
merged 19 commits into from
Aug 18, 2021
Merged

CSS adjustments in post-processed HTML manual #10497

merged 19 commits into from
Aug 18, 2021

Commits on Jul 20, 2021

  1. webman: Remove colored background for inline code 

    Looks incohesive in syntax descriptions, unlike in htmlman or pdf which
don't color the backgrounds.
    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    f8390bc View commit details
    Browse the repository at this point in the history

  2. webman: Follow inline code styling of htmlman 

    The color ocaml#888 has far too low contrast, I chose the color used for
links but darker.
    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    a194d25 View commit details
    Browse the repository at this point in the history

  3. webman: Italicize grammar symbol names 

    Chapter 9, The OCaml language:
"Non-terminal symbols are set in italic font"
    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    ef6d050 View commit details
    Browse the repository at this point in the history

  4. webman: Make display style blocks centered

    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    d5fe429 View commit details
    Browse the repository at this point in the history

  5. webman: Increase heading font-weight

    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    61764cc View commit details
    Browse the repository at this point in the history

  6. webman: Use SCSS variables for font-family

    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    8900ac5 View commit details
    Browse the repository at this point in the history

  7. webman: Set command-line arguments in monospace

    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    b4eb567 View commit details
    Browse the repository at this point in the history

  8. webman: Set (mathematical) variables in italics

    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    a50a4d4 View commit details
    Browse the repository at this point in the history

  9. webman: Remove styling for the ordinal "th" 

    The class .009 is used only for superscript "th" and it looked odd with
the colored background. Now it follows the LaTeX styling.
    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    cfd3c03 View commit details
    Browse the repository at this point in the history

  10. webman/api: Improve constructor color contrast 

    Now the .constructor class (used for data constructors and modules) uses
the same color as types.
    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    7c1fd96 View commit details
    Browse the repository at this point in the history

  11. webman: Center tables

    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    e311dab View commit details
    Browse the repository at this point in the history

  12. webman: Make table headers bold 

    Rules copied from htmlman
    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    afe24ba View commit details
    Browse the repository at this point in the history

  13. webman: Fix variables being bolded, not italicized 

    Rule based on htmlman CSS
    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    f6355cf View commit details
    Browse the repository at this point in the history

  14. webman: Add spacing to tables for aligned exprs 

    Rule copied from htmlman CSS
    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    cfb2545 View commit details
    Browse the repository at this point in the history

  15. webman: Add padding to .cellpadding1 

    Rule copied from htmlman CSS
    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    321a227 View commit details
    Browse the repository at this point in the history

  16. webman: Styling for Unix/Windows specific blocks 

    Similar to htmlman.
It's necessary to be able to see when Unix/Windows specific information
ends.  These blocks have to be styled differently, it's mentioned in the
foreword.
    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    27ae0f5 View commit details
    Browse the repository at this point in the history

  17. webman: Italicize command-line argument variables 

    Rule based on htmlman CSS
    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    d56cbd0 View commit details
    Browse the repository at this point in the history

  18. webman: Center BNF syntax bars | 

    Rule based on htmlman CSS
    @wikku
    wikku committed Jul 20, 2021
    Configuration menu
    Copy the full SHA
    49b9cd3 View commit details
    Browse the repository at this point in the history

Commits on Aug 17, 2021

  1. Add Changes entry

    @wikku
    wikku committed Aug 17, 2021
    Configuration menu
    Copy the full SHA
    9671c87 View commit details
    Browse the repository at this point in the history