` around ordinary Markdown, * and `{.class}` where a specific line needs naming. What that means in * practice, per component, is on the style page. * * Two conventions used throughout, stated once: * * 1. The type tokens are `em`-relative to the typeset base, so they compose: * an entry set at --type-small (0.8125em) whose title is --type-h3 * (1.1875em) puts the title at 0.965em -- just under body size -- against * 14px metadata. That compounding is deliberate and is the only way to * get a size hierarchy inside a component without inventing a token. * * 2. No component wraps itself in a link. A card whose whole surface is * clickable has to nest the title and action links inside that link, which * is invalid, unreachable by keyboard in the way it looks, and destroys * text selection. Cards are

s; the title and the action links are * ordinary sibling links, and each gets the global :focus-visible ring. * Nothing here sets `overflow: hidden`, so that ring is never clipped. */ /* ── project card ───────────────────────────────────────────────────────── * *

* **[title](url)** * * One-line summary. * * `Agda`{.tag} `Nix`{.tag} * * [Source](url) · [Docs](url) * {.project-links} *

* * Every part after the title is optional. The title is the first paragraph, * so it needs no class of its own; the links row needs one because it is * pinned to the bottom of the card, which is what keeps a row of cards of * different lengths aligned along their actions. */ .md-typeset .project-grid { display: grid; /* Half a text column is the point at which a card stops being a card and starts being a paragraph with a border, so that is the track minimum. `min(100%, …)` keeps a single card from overflowing a narrow viewport. */ grid-template-columns: repeat(auto-fit, minmax(min(100%, calc(var(--measure) / 2)), 1fr)); gap: var(--space-4); margin: var(--space-8) 0; } .md-typeset .project-card { display: flex; flex-direction: column; gap: var(--space-2); /* The anchor for the preview below (M3-3b, #97), which is a descendant of the card rather than a sibling: hovering a descendant hovers its ancestor whatever box it sits in, and that is what lets the pointer travel from the card onto the preview without the preview closing under it (WCAG 1.4.13, "hoverable"). */ position: relative; background-color: var(--c-bg-raised); border: var(--border-width) solid var(--c-line); border-radius: var(--radius-md); padding: var(--space-4); font-size: var(--type-small); color: var(--c-fg-muted); transition: border-color 120ms; } /* Hover and keyboard focus are deliberately different colours: hover is a passing pointer, focus is where the keyboard actually is. */ .md-typeset .project-card:hover { border-color: var(--c-line-strong); } .md-typeset .project-card:focus-within { border-color: var(--c-accent); } /* The open card paints over the ones after it. Without this the preview, which is a positioned descendant, is painted in tree order and therefore *under* every later card in the grid -- so the preview of a card in the first row disappeared behind the second row rather than over it. Only the open card is raised, so nothing else in the grid changes layer. */ .md-typeset .project-card:hover, .md-typeset .project-card:focus-within { z-index: 2; } /* The flex `gap` owns the vertical rhythm inside a card; Material's paragraph margins would otherwise be added to it. */ .md-typeset .project-card > * { margin: 0; } .md-typeset .project-card > p:first-child { font-family: var(--font-display), var(--font-body), sans-serif; font-size: var(--type-h3); font-weight: var(--display-weight); letter-spacing: var(--tracking-display); line-height: var(--leading-heading); color: var(--c-fg); } /* The title is authored as `**…**`, so the paragraph's weight is not the one that lands: `.md-typeset strong` sets its own, and it wins over inheritance. Under Constellation both tokens are 600 and nothing shows; under Meridian --display-weight is 500, and the card title would be the one component title that ignored it. Measured, not assumed: forcing --display-weight to 500 moves the publication title, the talk title and every heading to 500 and leaves this one at 600 without this rule. */ .md-typeset .project-card > p:first-child > strong { font-weight: var(--display-weight); } /* A title that links somewhere reads as a link; one that does not is still a title. The bottom rule under body links is noise at this size. */ .md-typeset .project-card > p:first-child a { border-bottom: none; } .md-typeset .project-links { /* Pushed to the bottom, so cards in a row line their actions up. */ margin-top: auto; padding-top: var(--space-2); } /* ── card preview ───────────────────────────────────────────────────────── * *

* … * *

* * The marker is expanded by scripts/python/preview_hook.py from * docs/assets/previews.json, which `make previews` writes: a 480x270 * thumbnail of the card's artifact -- a paper's first page, or the front * page of the site the card points at -- the facts gen_previews.py derived * about it, and a line saying what was photographed and when. A card with * no marker is exactly the card above, which is the floor this degrades to. * * Three decisions are worth stating, because each is the answer to a way * this component can be got wrong. * * 1. **It opens below the card, never over it, and in one column.** A * preview that covered the card would cover the card's own links, which * is the one thing it must not do, and one beside the card has nowhere * to go the moment the grid drops to a single column. Inside the * preview the answer is the same, for a measured reason: a card on the * projects page is 334px wide, and a 200px thumbnail beside the facts * leaves them 96px, at which every label wraps. Measured on that card, * the two-column preview came out 436px tall against the 337px the one * column gives it. One column at every width is one shape to keep * right. * * 2. **It is flush with the card, not floating near it.** The two borders * overlap into a single line, so the pointer crosses no gap on its way * in. A gap would un-hover the card mid-journey and take the preview * away before it could be read, which is the failure WCAG 1.4.13's * "hoverable" names. * * 3. **The pointer opens it only where there is a pointer.** A touch * browser reports `hover: none` and synthesises a sticky `:hover` on * tap; without the media query the first tap on a card would open a * preview across the next card instead of following the link. Keyboard * focus opens it everywhere, since that gesture means the same thing on * every device. * * Escape closes an open preview, which is the third WCAG requirement and the * one no selector can express: docs/javascripts/preview.js sets * `data-preview="dismissed"` on the card, the `:not()` below reads it, and * the mark is lifted when the pointer or the focus leaves. */ .md-typeset .card-preview { display: none; position: absolute; /* `top: 100%` is the card's *padding* box, one border width above its outer edge, so the two 1px borders land on each other as a single line and the pointer crosses no gap. */ top: 100%; left: 0; right: 0; /* The cap sits just under the thumbnail's own 480px, so the image is never shown larger than it was captured: on a wide card the preview stops here rather than becoming a billboard, and on a narrow one it is simply the card's width. */ max-width: 22rem; grid-template-columns: minmax(0, 1fr); gap: var(--space-2); padding: var(--space-3); background-color: var(--c-bg-raised); border: var(--border-width) solid var(--c-line-strong); /* Square where it meets the card, rounded where it leaves it: the pair reads as one object that grew, rather than two that collided. */ border-radius: 0 0 var(--radius-md) var(--radius-md); } .md-typeset .project-card:not([data-preview="dismissed"]):focus-within > .card-preview, .md-typeset .project-card-pinned > .card-preview { display: grid; } @media (hover: hover) { .md-typeset .project-card:not([data-preview="dismissed"]):hover > .card-preview { display: grid; } } .md-typeset .card-preview-shot { display: block; width: 100%; height: auto; border-radius: var(--radius-sm); /* The element carries the file's own width and height, so the box is the right size before the bytes arrive; this is what fills it until they do. The image is `loading="lazy"` and a preview has no box until it opens, so none of the six is fetched on a page load -- measured in Chromium, not assumed. */ background-color: var(--c-bg-sunken); } .md-typeset .card-preview-body { display: flex; flex-direction: column; gap: var(--space-2); min-width: 0; } .md-typeset .card-preview-facts { display: grid; grid-template-columns: auto minmax(0, 1fr); gap: var(--space-1) var(--space-3); margin: 0; /* A rem token, not an em one: the card is already at --type-small, and an em-relative size here would compound with it to something smaller than the site sets anywhere. */ font-size: var(--type-ui); } .md-typeset .card-preview-facts dt { margin: 0; font-weight: 400; color: var(--c-fg-faint); } .md-typeset .card-preview-facts dd { margin: 0; color: var(--c-fg); /* A DOI is one unbreakable token as far as the line breaker is concerned, and a card column is narrow. Breaking it is better than widening the grid track around it. */ overflow-wrap: anywhere; } .md-typeset .card-preview-src { /* Last line of the preview, pushed to its floor, so a preview with three facts and one with none end the same way. */ margin: auto 0 0; font-size: var(--type-ui-small); color: var(--c-fg-faint); } /* On the style page one card is pinned open, in flow rather than floating. * A component that is `display: none` everywhere it appears is one the * contrast and font audits never measure -- `offsetParent === null` is the * first thing both skip -- so the open state would ship unmeasured. This is * the one place it is pinned, and measuring it is the reason. */ .md-typeset .project-card-pinned > .card-preview { position: static; margin-top: var(--space-2); border-radius: var(--radius-md); } @media (prefers-reduced-motion: no-preference) { .md-typeset .card-preview { animation: card-preview-in var(--motion-preview) var(--motion-ease) both; } } @keyframes card-preview-in { from { opacity: 0; transform: translateY(calc(-1 * var(--space-2))); } } /* ── tag ────────────────────────────────────────────────────────────────── * * `Agda`{.tag} `invited`{.tag} `dormant`{.tag} * * A code span, because `attr_list` attaches to elements Markdown produces and * a bare `[text]{.tag}` is not one of them -- it renders literally. `em` and * `strong` were the alternatives and both already carry meaning here (venue, * emphasised author), so the neutral one is the right host. It is restyled * out of the code face: these are labels, not code. */ .md-typeset .tag { display: inline-block; /* An inline-block is a block container, so it inherits the hanging indent the publication and talk entries set and applies it to its own first line -- which slides the label out of its own border box. Caught by looking at a rendered talk entry with a tag on it, not by reading this. */ text-indent: 0; font-family: var(--font-body), sans-serif; font-size: var(--type-small); font-weight: 400; line-height: var(--leading-heading); color: var(--c-fg-muted); background-color: transparent; border: var(--border-width) solid var(--c-line-strong); border-radius: var(--radius-sm); padding: 0 var(--space-2); white-space: nowrap; } /* ── publication entry, talk entry, and secondary-project entry ─────────── * *

* - **Title** * Authors, with **William DeMeo** emphasised. *Venue*, **volume**:pages, year. * [DOI](url) · [arXiv:id](url) · [PDF](url) *

* * (each entry line ends with two spaces, so the lines stay one paragraph) * * A talk entry is the same grammar with a different second line -- venue, * location, year -- and the slides link on the title rather than in a row of * their own. They share these rules rather than being copies of each other, * because they are the same shape: a title, a line of attribution, and an * optional line of links. Where they differ, the rules are separated below. * * A secondary-project entry (#28) is the third consumer, and it is one line: * *

* - **[name](url)**: one sentence. `dormant`{.tag} *

* * It joins every rule above the two that promote the title, and takes neither * of those. That is the whole of the difference and it is deliberate. The * list sits under the project grid, so its names have to read as subordinate * to a card title; at --type-h3 in the display face they would be the same * size as one, and the section would compete with the grid instead of closing * it. Kept at the entry's own size the name is bold, accented and inline * with its sentence, and it keeps the faint underline every body link has, * which a display-size title drops as noise but a body-size name needs as its * only affordance. A name with nothing to link to is bold text, which is the * same floor a talk with no slides degrades to. * * The publication list is written by `gen_publications.py` from * `bibliography.json` (M5-1, #29): the generator emits exactly this Markdown * and knows nothing about these classes, so the page wraps its output and adds * nothing. Every optional part is optional in the generator too -- an entry * with no DOI, no arXiv identifier and no venue simply has fewer lines. */ .md-typeset .publications ul, .md-typeset .talks ul, .md-typeset .secondary ul { list-style: none; margin-left: 0; padding-left: 0; max-width: var(--measure); } .md-typeset .publications li, .md-typeset .talks li, .md-typeset .secondary li { margin: 0 0 var(--space-6); /* A hanging indent, the way a reference list has always been set. `text-indent` applies to the first line of the block only, and it is inherited, so it reaches the

that a loose list wraps each item in -- which is why this works whether or not the source has blank lines between entries. The lines after each
keep the padding. */ padding-left: var(--space-6); text-indent: calc(-1 * var(--space-6)); font-size: var(--type-small); color: var(--c-fg-muted); } .md-typeset .publications li:last-child, .md-typeset .talks li:last-child, .md-typeset .secondary li:last-child { margin-bottom: 0; } /* Material gives a list item inside a loose list its own paragraph margins. */ .md-typeset .publications li > p, .md-typeset .talks li > p, .md-typeset .secondary li > p { margin: 0; } /* The emphasised author -- and the volume number, which is marked up the same way -- steps forward out of the muted metadata. */ .md-typeset .publications li strong, .md-typeset .talks li strong, .md-typeset .secondary li strong { color: var(--c-fg); } .md-typeset .publications li > strong:first-child, .md-typeset .publications li > p:first-child > strong:first-child, .md-typeset .talks li > strong:first-child, .md-typeset .talks li > p:first-child > strong:first-child { font-family: var(--font-display), var(--font-body), sans-serif; font-size: var(--type-h3); font-weight: var(--display-weight); letter-spacing: var(--tracking-display); } /* A linked title is the artifact itself -- the slides, for a talk -- so it carries the accent. A talk with no slides is a title in plain text, and that is the whole of the degradation. */ .md-typeset .publications li > strong:first-child a, .md-typeset .publications li > p:first-child > strong:first-child a, .md-typeset .talks li > strong:first-child a, .md-typeset .talks li > p:first-child > strong:first-child a { border-bottom: none; } /* A publication or a talk is two or three lines and is spaced to be read one at a time; a secondary entry is one line, and eight of them spaced that way read as eight separate things rather than as a list. Everything else about the block is shared above. The `:last-child` rule wins over this one on specificity whatever the order, so the last entry still ends flush. */ .md-typeset .secondary li { margin-bottom: var(--space-3); } /* ── timeline entry ─────────────────────────────────────────────────────── * *

* 2023– * : **Formal Verification Engineer**, Formal Methods — [IO](url) * What the position actually was. *

* * A definition list, because that is what a timeline is: a date, and what * happened then. `def_list` is already enabled, the source reads as the thing * it describes, and the CV's education and grants sections are written this * way already -- wrapping them is the whole migration. * * An open-ended range is `2023–` with nothing after the dash, which needs no * support here beyond not assuming two dates. */ .md-typeset .timeline dl { display: grid; grid-template-columns: max-content 1fr; column-gap: var(--space-6); /* No row gap: the rule down the left of the second column is continuous only if the rows touch, so the spacing between entries is padding on the rows themselves. */ row-gap: 0; max-width: var(--measure-heading); margin: var(--space-8) 0; } /* No bottom padding here, deliberately. A grid row is as tall as its tallest item, so padding on the date would set the row height whenever it exceeded the entry's -- which is exactly the last row, where the entry's padding is removed. The stretched entry's rule would then hang below its own last line by the height of that padding. The spacing between rows is the entry's job alone; the date is one line and never the taller of the two. */ .md-typeset .timeline dt { grid-column: 1; margin: 0; /* Flush with the margin, not ragged against the entry: an open range such as `2023–` otherwise floats right of the closed ones above and below it (William, on review of #42). The PDF's date gutter is set the same way. */ text-align: left; font-size: var(--type-small); font-weight: 400; font-variant-numeric: tabular-nums; color: var(--c-fg-muted); } .md-typeset .timeline dd { position: relative; grid-column: 2; margin: 0; padding-left: var(--space-4); padding-bottom: var(--space-6); border-left: var(--border-width) solid var(--c-line); font-size: var(--type-small); color: var(--c-fg-muted); } .md-typeset .timeline dd:last-of-type { padding-bottom: 0; } /* The node on the line. Centred on the rule, and set against the first line of the entry rather than its middle, so entries of different heights line their dots up with their dates. */ .md-typeset .timeline dd::before { content: ""; position: absolute; top: var(--space-2); left: calc(-0.5 * (var(--space-1) + var(--border-width))); width: var(--space-1); height: var(--space-1); border-radius: 50%; background-color: var(--c-accent); } .md-typeset .timeline dd strong { color: var(--c-fg); } /* Material's mobile breakpoint. Below it the date gutter costs more width than it earns, so the entry stacks under its date and keeps the rule. */ @media screen and (max-width: 44.9375em) { .md-typeset .timeline dl { display: block; } .md-typeset .timeline dt { text-align: left; padding-bottom: var(--space-1); } } /* ── playground ─────────────────────────────────────────────────────────── * * The live Agda checker (M4-9b, #144). Everything below styles elements * that `playground.js` creates, with two exceptions: `.agda-exercise`, which * is a `

` in playground.md, and `.agda-exercise__gate`, which * `playground_hook.py` renders from the assets' manifest. Those two are the * page with JavaScript off, and they are styled to stand on their own rather * than to look like a widget waiting for its script. * * No motion. The only thing that moves is the download's ``, * which is state, so there is no reduced-motion branch here (ADR-009). */ .md-typeset .agda-exercise { margin: var(--space-8) 0; } /* The consent sentence. Set apart from the prose, because it is a claim * about what pressing the button costs and a reader skimming for the button * must not skim past it. */ .md-typeset .agda-exercise__gate { max-width: var(--measure); color: var(--c-fg-muted); font-size: var(--type-small); border-left: 2px solid var(--c-line-strong); padding-left: var(--space-4); margin: var(--space-4) 0; } .md-typeset .agda-exercise__controls, .md-typeset .agda-exercise__bar { display: flex; flex-wrap: wrap; align-items: center; gap: var(--space-3); margin: var(--space-4) 0; } /* The same control the proof terminal's replay is: a real