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.

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

Manual: improve typesetting and legibility of the HTML version #1741

Merged
merged 1 commit into from Apr 27, 2018

Conversation

Projects
None yet
7 participants
@steinuil
Copy link
Contributor

steinuil commented Apr 26, 2018

Some simple changes to the stylesheet of the manual to improve typesetting and legibility:

  • Long lines are very hard to read, so page width is now clamped to 800px which makes the lines about as wide as in the PDF version. I've also added a margin on the left (which disappears when the window shrinks) so it doesn't feel like it's been squeezed to the edge of the screen.
  • Line height was increased a bit, so that paragraphs don't feel too cramped. Some padding was also added to table cells for the same purpose.
  • Long lines in code blocks will now cause the block to display a horizontal scrollbar instead of overflowing. This doesn't change anything on desktop, but it might make reading on a phone a bit nicer.

Unfortunately some syntax definitions (such as those in Chapter 8) are still too wide and will overflow past the page width, but I don't think there's much that can be done to fix those without making bigger changes. I looked at the PDF manual for inspiration, but it looks like even there they just go off the page...

@pmetzger

This comment has been minimized.

Copy link
Member

pmetzger commented Apr 27, 2018

This is a really good simple set of changes!

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Apr 27, 2018

Would you have a way to upload an HTML page before and after this change somewhere, for visual comparison?

@nojb

This comment has been minimized.

Copy link
Contributor

nojb commented Apr 27, 2018

I think this is a very good change. I uploaded a version of the HTML manual "before" and "after" for comparison.

@xavierleroy

This comment has been minimized.

Copy link
Contributor

xavierleroy commented Apr 27, 2018

This looks very nice! I'm strongly in favor.

@Octachron

This comment has been minimized.

Copy link
Contributor

Octachron commented Apr 27, 2018

I am also in favor. @steinuil , I believe that you should add a change entry in the "Manual and documentation" section of Changes.

@steinuil steinuil force-pushed the steinuil:typesetting branch from 575ab64 to be6ba7d Apr 27, 2018

@steinuil

This comment has been minimized.

Copy link
Contributor Author

steinuil commented Apr 27, 2018

@Octachron added.

% Compact layout
\newstyle{body}{max-width:800px}
\newstyle{@media (min-width:900px)}{body\{margin-left:50px\}}
\newstyle{@media (min-width:1000px)}{body\{margin-left:100px\}}

This comment has been minimized.

@Khady

Khady Apr 27, 2018

Contributor

Could we have auto margins for left and right rather than 100px? It would center the body, which is more comfortable IMO.

\newstyle{@media (min-width:900px)}{body\{margin-left:auto;margin-right: auto;\}}

I think it would allow to remove the different conditions for the 900px and 100px min-width too.

This comment has been minimized.

@steinuil

steinuil Apr 27, 2018

Author Contributor

I'm hoping that in the future the manual will look more like Racket's, which I think looks better if the body is left-aligned, so this was partly in hope of making it visually consistent with (possible) future changes. I also think it looks better by itself. I don't particularly mind changing it if others like it better centered though.

This comment has been minimized.

@steinuil

steinuil Apr 27, 2018

Author Contributor

I uploaded a centered version, and here's the left-aligned one.

@gasche

gasche approved these changes Apr 27, 2018

Copy link
Member

gasche left a comment

Approved -- from the very positive feedback.

@steinuil, please tell us what you think on the centering vs. left-alignment choice. If your mind hasn't changed by doing the comparison, we can merge as is.

@steinuil

This comment has been minimized.

Copy link
Contributor Author

steinuil commented Apr 27, 2018

I think it's ok as it is.

Changes Outdated
@@ -31,6 +31,9 @@ Working version

### Manual and documentation:

- GPR#1741: manual, improve typesetting and legibility in HTML output
(steinuil)

This comment has been minimized.

@gasche

gasche Apr 27, 2018

Member

I would like to backport your change in the 4.07 branch, so that they effect the manual of the upcoming release. @steinuil, could you displace this Change entry to be part of the same section in the "OCaml 4.07" entry below?

@steinuil steinuil force-pushed the steinuil:typesetting branch from be6ba7d to e02b5eb Apr 27, 2018

html manual: improve typesetting and legibility
Make the pages narrower to avoid overly long lines,
increase line height to improve legibility.

@steinuil steinuil force-pushed the steinuil:typesetting branch from e02b5eb to 49abafc Apr 27, 2018

@pmetzger

This comment has been minimized.

Copy link
Member

pmetzger commented Apr 27, 2018

This is already a significant improvement. I'd suggest increasing the font size, say for argument:

font-size:18px

and, depending on the results, possibly increasing the line height, say:

line-height:1.6

By the way, DO NOT take this suggestion as meaning I think integrating @steinuil's changes should be delayed until we have perfection!

@xavierleroy

This comment has been minimized.

Copy link
Contributor

xavierleroy commented Apr 27, 2018

Never set an absolute font size in an HTML document. This is for users to choose using the mechanisms provided by their browsers. Line spacing (relative, of course) is open to debate, though.

@pmetzger

This comment has been minimized.

Copy link
Member

pmetzger commented Apr 27, 2018

Never set an absolute font size in an HTML document. This is for users to choose using the mechanisms provided by their browsers

Users can still increase and decrease the font size with their browser mechanisms, and can still override the sizes entirely, but this will provide a saner default. It is extremely rare that users change the default, so it is useful to pick good fonts and good point sizes.

@pmetzger

This comment has been minimized.

Copy link
Member

pmetzger commented Apr 27, 2018

(But again, I'd rather that merging the original change not be delayed by an attempt to achieve perfection. CSS styling can be tweaked more with time. @steinuil's change is a nice simple small fix that improves readability.)

@gasche gasche merged commit bb06a44 into ocaml:trunk Apr 27, 2018

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
@gasche

This comment has been minimized.

Copy link
Member

gasche commented Apr 27, 2018

Merged, and cherry-picked in 4.07 as ecf7234.

My own vague memories of CSS units suggest that em might be a more robust unit than px to use (especially if we decide to later change the default font size), but the px definition in fact looks more flexible (and baroque) than I remembered and there may not be such a difference anymore.

@steinuil

This comment has been minimized.

Copy link
Contributor Author

steinuil commented Apr 27, 2018

px is an absolute unit, while em is a relative one. Usually there's a root font size set in px in an html or body selector, and every other font size should be set using em (which makes it relative to the font size of the element's container), so if you want to resize all the fonts e.g. when the screen gets narrower, you just have to change the root size in a @media query.

I set the line height to em, so if the font size were to be increased the line height would increase accordingly.

@steinuil steinuil deleted the steinuil:typesetting branch Apr 27, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.