leanprover / doc-gen4

Document Generator for Lean 4
Apache License 2.0
62 stars 41 forks source link

Remove fixed font-size #173

Closed winstonyin closed 8 months ago

winstonyin commented 8 months ago
eric-wieser commented 8 months ago
  • The biggest text on the top left should be Mathlib4 rather than the non-descriptive Documentation. Size adjusted to h2.
  • The file name shown at the top is now grey to reduce visual fatigue. Size adjusted to h4

h1-h6 shouldn't be chosen based on size, but on hierarchy. Size is a style consideration best left of CSS

hargoniX commented 8 months ago

Apart from the mathlib specific changes this looks fine to me (but feel free to bikeshed on frontend as much as you like, I have no idea what's correct here). As for my opinion on the mathlib specific changes, I already explained that over here yesterday: https://github.com/leanprover/doc-gen4/pull/172#issuecomment-1879116753