/* File: docs/stylesheets/extra.css The agda-native-air site's styles (issue #169). Everything here is expressed in the tokens from tokens.css; there are no raw colors or sizes below this comment. That is the property that makes the visual system a system rather than a set of preferences: changing one token moves every place it is used, and nothing else can drift. Material is restyled through its own custom properties rather than by overriding its rules, which is the supported route and survives a theme upgrade. Where a rule is unavoidable it is because Material hard-codes a value that has no variable. Inherited from williamdemeo.org (the williamdemeo/website repository, docs/stylesheets/extra.css at fcb6bf0, 2026-09-20): the variable mapping, the syntax palette, the typography, the chrome, the search field, the tables, the admonitions, and the buttons, which together are what makes the two sites look like siblings. Left behind, because they style components this site does not have: that site's home hero, constellation, evidence strip, typed-proof terminal, project cards and previews, tags, publication and talk entries, and timeline. Load order matters and is set in mkdocs.yml: fonts.css declares the faces, tokens.css declares the values, this file applies them. */ /* == Material's variables, expressed in ours ================================ The selector is `[data-md-color-scheme]` rather than `:root` because that attribute lives on , which is also where tokens.css puts the color tokens. Mapping on :root would read them from an element that does not have them. */ [data-md-color-scheme] { /* JuliaMono is the last self-hosted entry in the text stack, not an afterthought: no text face carries ∀, ⊢, or ⨅, and a mathematical symbol that reaches prose should come from a font this site ships rather than from whatever the reader's machine offers. Material appends its own system fallbacks after whatever this names. */ --md-text-font: var(--font-body), var(--font-mono); --md-code-font: var(--font-mono); --md-default-bg-color: var(--c-bg); --md-default-bg-color--light: color-mix(in srgb, var(--c-bg) 70%, transparent); --md-default-bg-color--lighter: color-mix(in srgb, var(--c-bg) 30%, transparent); --md-default-bg-color--lightest: color-mix(in srgb, var(--c-bg) 12%, transparent); --md-default-fg-color: var(--c-fg); --md-default-fg-color--light: var(--c-fg-muted); --md-default-fg-color--lighter: var(--c-fg-faint); --md-default-fg-color--lightest: var(--c-line); --md-typeset-color: var(--c-fg); --md-typeset-a-color: var(--c-accent); --md-typeset-mark-color: var(--c-accent-wash); --md-typeset-del-color: color-mix(in srgb, var(--c-accent) 18%, transparent); --md-typeset-ins-color: color-mix(in srgb, var(--c-accent) 18%, transparent); --md-typeset-table-color: var(--c-line); --md-typeset-kbd-color: var(--c-bg-raised); --md-typeset-kbd-border-color: var(--c-line-strong); --md-typeset-kbd-accent-color: var(--c-bg); /* The header is paper with a hairline under it, not a block of color. That is most of what separates a 2026 documentation site from a 2016 one. */ --md-primary-fg-color: var(--c-bg); --md-primary-fg-color--light: var(--c-bg-raised); --md-primary-fg-color--dark: var(--c-bg-sunken); --md-primary-bg-color: var(--c-fg); --md-primary-bg-color--light: var(--c-fg-muted); --md-accent-fg-color: var(--c-accent-hover); --md-accent-fg-color--transparent: var(--c-accent-wash); --md-accent-bg-color: var(--c-on-accent); --md-accent-bg-color--light: var(--c-on-accent); --md-code-bg-color: var(--c-bg-raised); --md-code-fg-color: var(--c-fg); --md-footer-bg-color: var(--c-bg-sunken); --md-footer-bg-color--dark: var(--c-bg-sunken); --md-footer-fg-color: var(--c-fg); --md-footer-fg-color--light: var(--c-fg-muted); /* Material puts the "Made with ..." line in --lighter. The faint token is tuned to clear AA on the page surfaces, not on the darker footer band, so the footer gets the muted one instead of a fourth gray. */ --md-footer-fg-color--lighter: var(--c-fg-muted); /* No drop shadows anywhere. Depth is carried by a one-pixel line and a change of surface, which reads the same in both themes and does not need a different color for each. */ --md-shadow-z1: 0 0 0 1px var(--c-line); --md-shadow-z2: 0 0 0 1px var(--c-line); --md-shadow-z3: 0 0 0 1px var(--c-line-strong); } /* Syntax highlighting. Material's defaults are tuned to its own palettes and lose contrast against these surfaces, so the token colors are set from the palette instead. Keywords and strings carry the hue; everything else is a gray, because a code block where nine things are colored is a code block where nothing stands out. */ [data-md-color-scheme="default"] { --md-code-hl-color: var(--c-accent-wash); --md-code-hl-color--light: var(--c-accent-wash); --md-code-hl-keyword-color: #7c3aed; --md-code-hl-function-color: #1d4ed8; --md-code-hl-string-color: #15803d; --md-code-hl-number-color: #b45309; --md-code-hl-constant-color: #b45309; --md-code-hl-special-color: #be123c; --md-code-hl-operator-color: var(--c-fg-muted); --md-code-hl-punctuation-color: var(--c-fg-muted); --md-code-hl-name-color: var(--c-fg); --md-code-hl-variable-color: var(--c-fg); --md-code-hl-comment-color: var(--c-fg-faint); --md-code-hl-generic-color: var(--c-fg-muted); } [data-md-color-scheme="slate"] { --md-code-hl-color: var(--c-accent-wash); --md-code-hl-color--light: var(--c-accent-wash); --md-code-hl-keyword-color: #c4b5fd; --md-code-hl-function-color: #93c5fd; --md-code-hl-string-color: #86efac; --md-code-hl-number-color: #fcd34d; --md-code-hl-constant-color: #fcd34d; --md-code-hl-special-color: #fda4af; --md-code-hl-operator-color: var(--c-fg-muted); --md-code-hl-punctuation-color: var(--c-fg-muted); --md-code-hl-name-color: var(--c-fg); --md-code-hl-variable-color: var(--c-fg); --md-code-hl-comment-color: var(--c-fg-faint); --md-code-hl-generic-color: var(--c-fg-muted); } /* == typography ============================================================= */ .md-typeset { font-size: var(--type-base); line-height: var(--leading-body); letter-spacing: var(--tracking-body); } .md-typeset h1, .md-typeset h2, .md-typeset h3, .md-typeset h4 { font-family: var(--font-display), var(--font-body), var(--font-mono), sans-serif; color: var(--c-fg); letter-spacing: var(--tracking-display); line-height: var(--leading-heading); text-wrap: balance; } .md-typeset h1 { font-size: var(--type-h1); font-weight: var(--display-weight); margin: 0 0 var(--space-8); } .md-typeset h2 { font-size: var(--type-h2); font-weight: var(--display-weight); margin: var(--space-16) 0 var(--space-4); padding-bottom: var(--space-2); border-bottom: var(--border-width) solid var(--c-line); } .md-typeset h3 { font-size: var(--type-h3); font-weight: var(--strong-weight); margin: var(--space-12) 0 var(--space-3); } .md-typeset h4 { font-size: var(--type-h4); font-weight: var(--strong-weight); letter-spacing: var(--tracking-body); margin: var(--space-8) 0 var(--space-2); } .md-typeset h5 { font-size: var(--type-small); font-weight: var(--strong-weight); letter-spacing: var(--tracking-caps); text-transform: uppercase; color: var(--c-fg-muted); } .md-typeset strong, .md-typeset b { font-weight: var(--strong-weight); } /* Line length. Only the prose blocks are capped, and only where they are direct children of the article: a paragraph inside a table cell or an admonition already has a container deciding its width. */ .md-typeset > p, .md-typeset > ul, .md-typeset > ol, .md-typeset > dl, .md-typeset > blockquote { max-width: var(--measure); } .md-typeset > h1, .md-typeset > h2, .md-typeset > h3, .md-typeset > h4 { max-width: var(--measure-heading); } .md-typeset p { margin: 0 0 var(--space-6); } .md-typeset blockquote { border-left: 2px solid var(--c-line-strong); color: var(--c-fg-muted); padding-left: var(--space-4); } .md-typeset hr { border-bottom: var(--border-width) solid var(--c-line); margin: var(--space-16) 0; } /* Links: colored, and underlined only on hover. A page of prose with a permanent underline under every citation is noisier than it is helpful, but color alone is not a sufficient affordance, so the underline appears on hover and focus and the color clears AA on its own. */ .md-typeset a { text-decoration: none; border-bottom: var(--border-width) solid color-mix(in srgb, var(--c-accent) 35%, transparent); transition: border-color 120ms, color 120ms; } .md-typeset a:hover, .md-typeset a:focus-visible { color: var(--c-accent-hover); border-bottom-color: var(--c-accent); } /* Headings own their permalinks; the anchor should not read as a body link. */ .md-typeset .headerlink { border-bottom: none; } :focus-visible { outline: 2px solid var(--c-accent); outline-offset: 2px; } /* == code =================================================================== */ .md-typeset code, .md-typeset pre > code, .md-typeset kbd { font-family: var(--font-mono), monospace; font-size: var(--type-code); /* Only JuliaMono Regular is shipped: the syntax theme is color-only, so no bold or italic code face is ever needed. Pinning the weight stops a `code` inside a heading asking for 600 and getting a synthesized bold. */ font-weight: 400; font-variant-ligatures: none; } .md-typeset code { background-color: var(--c-bg-raised); border-radius: var(--radius-sm); padding: 0.1em 0.3em; } .md-typeset pre > code { padding: var(--space-4); line-height: 1.6; } .md-typeset .highlight, .md-typeset .highlighttable { border: var(--border-width) solid var(--c-line); border-radius: var(--radius-md); overflow: hidden; } .md-typeset .highlight code { background: transparent; } /* == chrome ================================================================= */ .md-header { box-shadow: none; border-bottom: var(--border-width) solid var(--c-line); } .md-header--shadow { box-shadow: none; } .md-tabs { border-bottom: var(--border-width) solid var(--c-line); } .md-nav { font-size: var(--type-ui); } .md-nav__title { color: var(--c-fg-muted); font-weight: var(--strong-weight); letter-spacing: var(--tracking-caps); text-transform: uppercase; font-size: var(--type-ui-small); } /* Search. Material builds the field out of hsla(0,0%,100%,.12) over the primary color, which assumes the header is a block of color. Against paper it is a gray slab, so the field is restated as a bordered surface. */ .md-search__form { background-color: var(--c-bg-raised); border: var(--border-width) solid var(--c-line); border-radius: var(--radius-md); box-shadow: none; } .md-search__form:hover { background-color: var(--c-bg-sunken); } .md-search__input, .md-search__icon { color: var(--c-fg); } .md-search__input::placeholder { color: var(--c-fg-muted); } [data-md-toggle="search"]:checked ~ .md-header .md-search__form { background-color: var(--c-bg); border-color: var(--c-line-strong); } .md-search__output { border: var(--border-width) solid var(--c-line); border-radius: var(--radius-md); box-shadow: none; } .md-footer-meta { border-top: var(--border-width) solid var(--c-line); } .md-typeset table:not([class]) { border: var(--border-width) solid var(--c-line); border-radius: var(--radius-md); font-size: var(--type-small); } .md-typeset table:not([class]) th { background-color: var(--c-bg-raised); font-weight: var(--strong-weight); } /* Material renders the search overlay and the admonition titles with a tint derived from the accent; keep those on the palette too. */ .md-typeset .admonition, .md-typeset details { border: var(--border-width) solid var(--c-line); border-radius: var(--radius-md); box-shadow: none; font-size: var(--type-small); } .md-typeset .md-button { /* Material builds its buttons out of --md-primary-fg-color, which here is the paper color, so the default rule is white on white. They are restated from the palette rather than patched. */ color: var(--c-fg); border: var(--border-width) solid var(--c-line-strong); border-radius: var(--radius-md); font-weight: var(--strong-weight); padding: var(--space-2) var(--space-4); transition: background-color 120ms, color 120ms, border-color 120ms; } .md-typeset .md-button--primary, .md-typeset .md-button:hover, .md-typeset .md-button:focus-visible { background-color: var(--c-accent); border-color: var(--c-accent); color: var(--c-on-accent); } /* Admonitions. Material gives each of its dozen types a hard-coded hue, which is a lot of color for a page that is meant to have one. The informational types are folded onto the accent; the ones that mean "be careful" keep their semantic color, because that is what they are for. */ .md-typeset .admonition.note, .md-typeset .admonition.info, .md-typeset .admonition.abstract, .md-typeset .admonition.tip, .md-typeset .admonition.example, .md-typeset .admonition.quote, .md-typeset details.note, .md-typeset details.info, .md-typeset details.abstract, .md-typeset details.tip, .md-typeset details.example, .md-typeset details.quote { border-color: var(--c-line); border-left: 2px solid var(--c-accent); } .md-typeset .note > .admonition-title, .md-typeset .info > .admonition-title, .md-typeset .abstract > .admonition-title, .md-typeset .tip > .admonition-title, .md-typeset .example > .admonition-title, .md-typeset .quote > .admonition-title, .md-typeset .note > summary, .md-typeset .info > summary, .md-typeset .abstract > summary, .md-typeset .tip > summary, .md-typeset .example > summary, .md-typeset .quote > summary { background-color: var(--c-accent-wash); color: var(--c-fg); } .md-typeset .note > .admonition-title::before, .md-typeset .info > .admonition-title::before, .md-typeset .abstract > .admonition-title::before, .md-typeset .tip > .admonition-title::before, .md-typeset .example > .admonition-title::before, .md-typeset .quote > .admonition-title::before, .md-typeset .note > summary::before, .md-typeset .info > summary::before, .md-typeset .abstract > summary::before, .md-typeset .tip > summary::before, .md-typeset .example > summary::before, .md-typeset .quote > summary::before { background-color: var(--c-accent); }