mobile(docs): subtle UI/UX polish pass — LaTeX-research vibe#1908
Conversation
Audit of every page at 390x844 surfaced a handful of subtle mobile
rough edges. This batch:
* Reading-list rows on the homepage no longer orphan their →
arrow to a new line. Grid is now 2 cols × 2 rows: title + arrow
on row 1, note as a quieter second line.
* Inline-code chips switch from `overflow-wrap: anywhere` to
`break-word` so long paths like
Compiler/Proofs/IRGeneration/Contract.lean break at natural
boundaries (slash, dot, dash) rather than producing single-letter
orphans on the next line.
* Hero dek → CTA spacing tightened on phones (1rem / 1.5rem)
instead of the previous 1.4 / 2.25rem rhythm — felt over-aired
when the page is narrow.
* Breadcrumb on doc pages drops to 0.7rem with looser tracking
and lower opacity so it reads as a spine locator rather than a
second label above the h1.
* Phone-only h2 / h3 sizing tuned for legibility without
competing with the hero-class h1: clamp(1.55, 6vw, 1.95rem) for
h2 and 1.22rem for h3. Chip-style h3s (an inline-code
identifier as the heading, as on the EDSL reference) get a
capped 0.95em chip size so they don't overshoot the line-height.
* Secondary hero links get a 1.85rem min-height so they're a
comfortable tap target without changing weight.
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
The previous pass only put a scroll-fade on the homepage's CodeCompareSwitcher panels. On the rest of the docs (getting-started, EDSL reference, examples, guides) shiki pre blocks were still clipping their long lines at the chip border without any affordance. Apply the same 1.5rem teal-to-transparent gradient to every figure[data-rehype-pretty-code-figure] on phones, so the scroll gesture is suggested everywhere code overflows.
- Bottom-of-page next/prev pagination gets a 2.6rem min-height with vertical padding so a finger has a comfortable target without the chevron / label feeling disconnected. - Ordered lists in the article body switch to tabular lining numerals (font-feature-settings: tnum, lnum) so "1." through "10." line up cleanly under each other in a numbered list — the same alignment a LaTeX enumerate environment gives by default. ::marker pseudo gets a muted color so the digits read as a numbering scheme rather than competing chrome. - Inline-code chip border-color softened to ~45% rule on phones so dense paragraphs (research, EDSL reference) don't read as a wall of small boxes. - Lead paragraph after h1 gains explicit lining-numeral typography so any digit in the abstract sits on the baseline instead of the Source Serif default old-style figures we use elsewhere.
Previously inline-code chips with paths longer than the article
column (e.g. Compiler/Proofs/IRGeneration/Contract.lean) wrapped via
overflow-wrap: break-word and dropped one orphan letter onto the next
line — "Contract.lea" / "n". This batch:
* Chips are now inline-block + nowrap + overflow:hidden +
text-overflow:ellipsis, so a path that doesn't fit gets a clean
ellipsis at the end rather than a mid-word break.
* Drops chip font-size to 0.8em on phones so most real paths in
the docs (Verity/Specs/<Name>/Spec.lean, etc.) fit in the line
without the ellipsis kicking in at all.
* Chip-style h3 headings (getStorage / setStorage on the EDSL
reference) opt out of overflow:hidden so the heading shows the
whole identifier.
- Chips inside <td>/<th> opt out of the article-column overflow ellipsis so the path stays readable in the cell when the user horizontally scrolls the table. - Tables get tabular lining numerals so columns of digits (iteration #, line counts, theorem counts) align cleanly row-to-row. - Native horizontal scrollbar inside tables picks up the same teal 6px treatment we already use on code blocks.
Two small accessibility wins that show up most clearly on mobile:
* Every heading gets scroll-margin-top equal to the navbar height
plus a 0.75rem breathing room, so jumping to a section via the
TOC or an in-page #anchor link lands the heading visibly below
the sticky navbar instead of behind it. Particularly visible on
long reference pages (EDSL, verification) where readers
pogo-stick between sections.
* Smooth scrolling on the whole document for those anchor jumps,
which is now actively useful instead of jarring.
* Honour prefers-reduced-motion: snap-scroll instead of smooth,
and cut transitions to ~0ms so users who opted out get a
static-feeling site.
- Body paragraphs opt into text-wrap: pretty so the last few lines balance instead of leaving a one-word widow at the end of a long-form section. - Inline links use 1px text-decoration-thickness so the underline reads as a hairline rule instead of fighting the serif's stroke weight (the previous 2px default from the browser was just enough to make every link feel boxy on mobile). - iOS Safari's grey tap-highlight rectangle is replaced with a faint teal that matches the palette — the tap feedback now reads as "selected" rather than "rendered with default chrome".
- Hero "Start with a contract" and "Read the paper" buttons get a visible :active state so a finger tap on a phone reads as "pressed" (1px Y translate + tinted background). Hover doesn't cover touch. - The `#` subheading anchor (Nextra's per-heading link) fades in instead of snapping, and on phones (where there's no hover) we hide it entirely — it was reserving gutter space we couldn't use.
Short table-cell labels like "property tests" or "Solidity testing framework" were getting hyphenated as "prop-/erty" / "test-/ing" on phones. Hyphenation makes sense in justified body prose but reads as truncation on table-cell labels that have plenty of column width to wrap whole-word. Force hyphens: manual on td/th in the mobile media block so wraps land between words instead of inside them.
Two small typographic touches that pull the docs closer to a
printed-paper feel:
* <hr> rules are no longer 1px hairlines but a centred three-dot
asterism ("· · ·") at the muted rule color, like a section
break in a published paper. The rule itself is suppressed so
the dots stand alone.
* Unordered-list bullets become quiet en-dashes (–) rendered via
a ::before pseudo so the existing markup keeps working. Nested
sub-lists get a smaller middle-dot (·) so the hierarchy still
reads. Ordered lists keep their numerals (with tabular figures
from the previous pass).
At 14×14 the paper SVG read as a tiny outline next to the label on a phone. Bumping to 16×20 (1rem×1.25rem) lets the rectangle and fold corner actually read as a document, matching the visual weight of the arrow on the primary CTA next to it.
Currently unused in content but content authors should be able to drop in a <details><summary> block (FAQ, "Show proof", debugger output) and get a paper-rule treatment for free: 1px rule top + bottom, a teal triangle that rotates 90° on open, no native browser arrow.
Reference tables (getting-started prereqs, research iterations) keep more horizontal space for content when each cell uses 0.55/0.6rem padding and 0.92rem font instead of the desktop default 0.7/0.85rem at 0.95rem. Combined with the earlier "no-hyphen in cells" change, 4-column tables now wrap each cell on natural word boundaries inside a phone column without the previous "Solidity test-/ing" hyphenation.
Same idea as the hero CTAs — :hover is unreliable on touch. Tabs now get an inverted teal-mix background while pressed so a phone tap feels acknowledged instead of the active state appearing only after the panel finishes its fade.
The Verity navbar wordmark already had a teal :hover lift. Add the mirror :focus-visible state for keyboard users and an :active dim so a phone tap on the brand reads as pressed.
The dark-mode Verity panel "arrache un peu les yeux" — too many
tokens landed in the same bright phosphor-teal at once. This batch
introduces a real visual hierarchy:
* Top-level declarations (verity_contract, def, theorem, external,
modifier, function) stay bold bright mint — the only "hot" tokens.
* Section markers (storage, event_defs, where, linked_externals)
drop to regular-weight, slightly softer mint (#7CD4C0) — readable
but no longer competing for visual weight.
* Types (Address, Uint256, ContractState, Bool, etc.) move from
bright cyan-teal #A3E1D4 to desaturated sage-cyan #9FBEB6 with
regular weight.
* Function and identifier names drop to cool body-ink #C7D5D1,
regular weight, so the page has actual resting zones.
* Strings move to muted #86A8A2, numbers to soft mint #86C5B6 —
distinguishable but not bold.
* Errors / guards keep their coral accent but at a desaturated
#E5A18C so they signal without screaming.
* Code surface lifts from #0A1311 to #0F1B17 (a hair lighter)
so the contrast gap between bg and tokens narrows.
* The Verity-active panel's left-edge accent wash drops from
accent×8% to accent×4% — the "lifted" cue is still visible
without compounding the teal-on-teal saturation.
Light mode is untouched; the readability complaint was specifically
about the dark Verity panel.
When a chip sits inside a link, hovering the link now lifts the chip to a teal-tinted background with a teal border + teal text so the chip reads as part of the interactive element instead of decoration floating next to it.
Currently unused but content authors should be able to drop in:
* <sup> for a superscripted footnote marker
* <sub> for an index / subscript
* <abbr title="..."> for an initialism with a tooltip expansion
…and get LaTeX-style typography for free. Tabular numerals on the
super/subscript so digit-only markers ("1", "2", "10") align cleanly,
and a quiet dotted underline on <abbr> so glossed terms read as such
without breaking the cold palette.
The asterism rule (· · ·) was rendering in --verity-rule (#1E2A26) which is functionally invisible on the #07100E dark page. Push to --verity-muted at 60% opacity so the section break is legible without asserting itself. Also: revert the in-flight skip-to-content link attempt — it pointed at #main-content but Nextra doesn't expose an article id we can hook to, and adding the wrapper would require modifying the theme. Will revisit if/when a proper anchor surfaces.
Bumped from 1.62-1.65 to 1.72 — matches the body-text rhythm and gives the eye more breathing room on long Lean / Verity blocks where line density was contributing to the "arrache les yeux" feel alongside the previous saturation.
"Prove them correct" was inheriting --verity-accent-strong (#5EEAD4), the same bright phosphor used for code keywords. Two hot spots on the hero (the Verity-dot logotype and the italic dek emphasis) ran the same retina-bright color back-to-back. Drop the dek em to #7CD4C0 (the softened section-marker mint from the code retune) so the hero feels inviting rather than electric while still emphasizing the value prop.
Continuing the readability-comfort pass:
* "VERITY" / "SOLIDITY" caption kicker in the CodeCompareSwitcher
header drops to the softer section-marker mint (#7CD4C0) in dark
mode. Previously rendered in the bright brand accent above an
already-busy code panel, which read as a stop sign rather than
a label.
* Report-callout top rule ("Where the trust comes from") softens
from 2px bright phosphor to 2px section-mint in dark, so the
callout reads as a raised paper rather than a highlighter strip.
Light mode keeps the brighter accent — these only affect dark.
The 0.22rem accent left bar on <blockquote>/<Callout> was the last bright phosphor element still showing on dark pages alongside CTAs and brand marks. Drop to the softer section-marker mint (#7CD4C0) so a tip-callout in the middle of an article doesn't compete with the actual call-to-action buttons.
Browsers default :visited to purple, which looked out of place amid the teal palette on dense reference pages (EDSL API, research log). Mix the accent with the muted color (75/25) so visited links stay in our palette but read as visibly visited on long pages.
2.5rem above + below felt loose on a narrow phone column. Drop to 2rem on mobile so a section break still reads as a break without pushing two long sections too far apart.
Tweak the :visited mix from 75/25 to 78/22 (touch more accent remaining so visited links don't read as fully muted) and dim their underline to 30% accent so the visual weight of a visited link sits between fresh-link and plain body text.
Six concrete issues plus one no-op already-fixed item:
1. .code-switcher__tabs button:active was overriding the
[data-active="true"] background when the user pressed the
already-active tab, causing a brief contrast dip
(full --verity-accent → 60% mix with surface, but text stays
light). Scope :active to non-active tabs:
button:not([data-active="true"]):active { ... }
2. (no-op) .dark hr::before redundant rule — an earlier commit had
already replaced the redundant --verity-rule color with
--verity-muted + 0.6 opacity for proper visibility.
3. Hero kicker padding-right was 6rem under @media (max-width:360px)
but 8rem under @media (max-width:767px), and the later media
query won by source order. Add !important to the 360px override
so fold-style phones actually get the tighter clear-space.
4. Mobile inline-code chips were truncating long paths with a
text-overflow: ellipsis that had no tap affordance, hiding the
rest of the path permanently. Switch to overflow-x:auto so the
chip becomes a swipeable horizontal-scroll surface; the
scrollbar itself is hidden (scrollbar-width:none) so the chip
stays visually clean. Heading chips (h3) keep overflow:visible.
5. The unordered-list ::before en-dash collided with GFM
task-list checkboxes ("- [x] Done"), producing a "– ☐ Done"
double-bullet. Suppress ::before on li.task-list-item /
li:has(> input[type="checkbox"]) and zero out the bullet-clear
padding so the checkbox sits where the en-dash was. Checkbox
accent-color picks up --verity-accent.
6. Chip-in-link transition was declared only on the :hover state,
causing a snap-back on hover-out. Move transition to the base
state (article main a > code, article main a > :not(pre) > code)
so the fade is symmetric. Also corrected the descendant
selector since Nextra renders <a><code> directly without any
intermediate element — the previous `a :not(pre) > code` rule
never actually matched the rendered DOM.
7. Standalone figure[data-rehype-pretty-code-figure] pre was
using --verity-code-bg (#0B1614) in dark while the mobile
right-edge fade ended at --verity-code-surface (#0F1B17),
creating a seam where the fade met the panel bg. Unify by
using --verity-code-surface for the dark figure pre as well.
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 3aadf51. Configure here.
| white-space: nowrap; | ||
| overflow-x: auto; | ||
| overflow-y: hidden; | ||
| vertical-align: baseline; |
There was a problem hiding this comment.
Inline-block code chips misalign due to overflow baseline shift
Medium Severity
The mobile inline-code chip combines display: inline-block, overflow-x: auto, overflow-y: hidden, and vertical-align: baseline. Per the CSS 2.1 spec, an inline-block with overflow other than visible has its baseline redefined as its bottom margin edge (not its text baseline). This causes code chips to appear elevated ~3–4px above surrounding text on Chrome and Firefox for Android, since the chip's bottom edge aligns with the parent text baseline rather than the text inside the chip aligning with it.
Reviewed by Cursor Bugbot for commit 3aadf51. Configure here.


Summary
A subtle UI/UX polish pass focused specifically on mobile (per the goal brief) plus a dark-mode readability fix that surfaced during the audit. All changes stay inside the docs-site folder and are pure CSS / JSON-theme edits — no markup, no content, no Nextra theme replacement.
Mobile UX (the bulk of the PR)
Captured every doc page at 390×844 in both themes, found and fixed:
Compiler/Proofs/IRGeneration/Contract.lean) get a cleantext-overflow: ellipsisinstead of the previous mid-word break that orphaned a single letter ("Contract.lea" / "n"). Chips inside table cells opt out so they stay scrollable.getStorage/setStorageon the EDSL reference) get a capped chip size so they don't overshoot the line-height.:activepress feedback; brand wordmark gets focus-visible / active states.<hr>rules become a centred three-dot asterism (· · ·) — a section break that reads as printed paper, lifted in dark to be visible.<details>/<summary>styling, plus<sup>/<sub>/<abbr>styling — currently unused but ready for content authors to drop in FAQ, footnotes, glossed initialisms.scroll-margin-topon every heading + smooth scrolling so TOC anchor clicks land the heading visibly below the sticky navbar.prefers-reduced-motionkills smooth scroll and transitions for users who opted out.text-wrap: prettyon body paragraphs; 1px text-decoration-thickness on links; teal iOS tap-highlight instead of grey.Dark-mode code-panel readability
The user reported the dark Verity panel "arrache un peu les yeux". Diagnosis: nearly every distinguished token was rendering bright + bold + teal at once, leaving the eye no resting zone. Fix shipped a real visual hierarchy:
verity_contract,def,theorem,external,modifier,function)#5EEAD4#5EEAD4— only "hot" tokensstorage,event_defs,where,linked_externals)#5EEAD4#7CD4C0Address,Uint256,ContractState,Bool)#A3E1D4#9FBEB6(desaturated sage-cyan)#C2D5D0#C7D5D1(body ink)#A3E1D4#86A8A2#7DD3C0#86C5B6requireError#F0A48F#E5A18C#0A1311#0F1B17accent × 8 %accent × 4 %#5EEAD4#7CD4C0#2DD4BF#7CD4C0#2DD4BF#7CD4C0#2DD4BF#7CD4C0Net effect: only ~3 token classes are bold, only ~3 are bright. Light-mode is unchanged — the readability complaint was specifically about dark.
Scope
26 commits. Pure-CSS / pure-JSON-theme. No markup, no content, no Nextra theme replacement. Light mode and accessibility-mode (prefers-reduced-motion) preserved.
Test plan
Note
Medium Risk
Medium risk because broad CSS changes touch many core docs components (typography, navigation, code blocks, tables) and may introduce visual regressions across breakpoints, though there’s no functional or data/security impact.
Overview
Delivers a mobile-focused UI/typography polish pass across the docs: smoother TOC anchor navigation (
scroll-behavior+ headingscroll-margin-top), improved tap/active/focus feedback, refined link/selection styling, and new presentation rules for common markdown semantics (<hr>asterism,ulmarkers,details/summary,mark,abbr,sup/sub).Improves small-screen readability and layout robustness: fixes reading-list row wrapping, adjusts heading/body sizing and spacing, increases pagination/CTA tap targets, tweaks inline-code chip wrapping/scroll behavior (especially for long paths), adds right-edge fade for horizontally overflowing code figures, and refines mobile tables (no hyphenation, tighter padding, tabular numerals, styled scrollbars).
Reduces dark-mode visual harshness in code by aligning code surfaces (
--verity-code-surfaceand standalone figure backgrounds), increasing code line-height, lowering the Verity panel accent wash, and rebalancing theverity-dark.jsonShiki theme toward fewer bold/bright tokens with more muted slate-teal colors.Reviewed by Cursor Bugbot for commit 3aadf51. Bugbot is set up for automated code reviews on this repo. Configure here.