From 027f7147be6786c588cabdd869027d23c344b762 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 9 Oct 2025 23:52:51 -0600 Subject: [PATCH 1/2] first pass at hover-over --- .../static/md/mkdocs/docs/css/agda-hover.css | 146 ++++++++ .../static/md/mkdocs/docs/js/agda-hover.js | 349 ++++++++++++++++++ build-tools/static/md/mkdocs/mkdocs.yml | 2 + 3 files changed, 497 insertions(+) create mode 100644 build-tools/static/md/mkdocs/docs/css/agda-hover.css create mode 100644 build-tools/static/md/mkdocs/docs/js/agda-hover.js diff --git a/build-tools/static/md/mkdocs/docs/css/agda-hover.css b/build-tools/static/md/mkdocs/docs/css/agda-hover.css new file mode 100644 index 000000000..5308751dd --- /dev/null +++ b/build-tools/static/md/mkdocs/docs/css/agda-hover.css @@ -0,0 +1,146 @@ +/* === Agda hover tooltip ================================================== */ +.agda-tooltip { + position: absolute; + z-index: 2000; + max-width: min(42rem, 92vw); + box-shadow: 0 10px 26px rgba(0,0,0,.18), 0 4px 10px rgba(0,0,0,.12); + border-radius: .5rem; + border: 1px solid rgba(0,0,0,.1); + backdrop-filter: blur(6px); + -webkit-backdrop-filter: blur(6px); + transition: opacity .12s ease, transform .12s ease; + transform: translateY(-2px); + opacity: 1; +} +.agda-tooltip.hidden { opacity: 0; pointer-events: none; } + +.agda-tooltip .agda-tooltip-inner { + padding: .75rem .9rem .7rem .9rem; + font-size: .92rem; + line-height: 1.25rem; +} + +.agda-tip-head { + display: flex; + align-items: baseline; + gap: .5rem; + margin-bottom: .4rem; + font-weight: 600; +} + +.agda-kind { + font-size: .78rem; + text-transform: uppercase; + letter-spacing: .06em; + opacity: .8; +} + +.agda-name { + font-family: ui-monospace, SFMono-Regular, Menlo, Monaco, Consolas, "Liberation Mono", "Courier New", monospace; + font-weight: 700; +} + +.agda-module { + margin-left: auto; + font-size: .78rem; + opacity: .7; +} + +.agda-tip-snippet { + white-space: pre-wrap; + margin: .25rem 0 .5rem 0; + padding: .5rem .6rem; + border-radius: .4rem; + background: rgba(127,127,127,.08); + font-size: .85rem; + overflow: hidden; +} + +.agda-tip-empty { + margin: .25rem 0 .5rem 0; + font-size: .85rem; + opacity: .85; +} + +.agda-tip-actions { + display: flex; + justify-content: flex-end; +} +.agda-open-def { + text-decoration: none; + font-weight: 600; +} + +/* Light/dark theming with MkDocs Material */ +:root, +[data-md-color-scheme="default"] { + --agda-tip-bg: #ffffff; + --agda-tip-fg: #1f2328; + --agda-tip-link: #0969da; + --agda-tip-border: rgba(0,0,0,.1); +} +[data-md-color-scheme="slate"] { + --agda-tip-bg: #1f2430; + --agda-tip-fg: #f4f6f8; + --agda-tip-link: #8ab4ff; + --agda-tip-border: rgba(255,255,255,.14); + .agda-tip-snippet { background: rgba(255,255,255,.06); } +} + +.agda-tooltip { + background: var(--agda-tip-bg); + color: var(--agda-tip-fg); + border-color: var(--agda-tip-border); +} +.agda-open-def { color: var(--agda-tip-link); } +/* === Agda tooltip polish (compact & clean) =============================== */ +.agda-tooltip .agda-tooltip-inner { + padding: .55rem .7rem .55rem .7rem; + font-size: .88rem; /* smaller base */ + line-height: 1.2rem; +} + +.agda-tip-head { + gap: .4rem; + margin-bottom: .25rem; + font-weight: 600; +} + +.agda-kind { + font-size: .72rem; + letter-spacing: .05em; + opacity: .75; +} + +.agda-name { + font-size: .9rem; /* tighter monospace name */ + font-weight: 700; +} + +.agda-module { + font-size: .72rem; + opacity: .6; +} + +.agda-tip-snippet { + margin: .2rem 0 .4rem 0; + padding: .45rem .55rem; + border-radius: .35rem; + font-size: .82rem; /* smaller code */ + line-height: 1.15rem; + max-width: 80ch; /* avoid ultra-wide lines */ + overflow-x: auto; /* allow horizontal scroll if needed */ + white-space: pre; /* preserve formatting exactly */ +} + +.agda-tooltip { + max-width: min(46rem, 92vw); /* a bit narrower overall */ + border-radius: .45rem; + box-shadow: 0 10px 22px rgba(0,0,0,.16), 0 3px 8px rgba(0,0,0,.10); + transform: translateY(-1px); +} + +/* Dark mode nuance */ +[data-md-color-scheme="slate"] .agda-tip-snippet { + background: rgba(255,255,255,.04); +} diff --git a/build-tools/static/md/mkdocs/docs/js/agda-hover.js b/build-tools/static/md/mkdocs/docs/js/agda-hover.js new file mode 100644 index 000000000..8a13cb743 --- /dev/null +++ b/build-tools/static/md/mkdocs/docs/js/agda-hover.js @@ -0,0 +1,349 @@ +// === Agda hover definitions =============================================== +// Works on Agda-generated HTML embedded in your Markdown, i.e., inside 
.
+// Shows a tooltip on hover with (1) token info, (2) link to full definition,
+// and (best-effort) a short snippet from the target page near the anchor.
+
+(function () {
+  const HOVER_SELECTOR = 'pre.Agda a[href]';       // limit to Agda pre blocks
+  const HOVER_DELAY_MS = 120;                      // small debounce to avoid flicker
+  const MAX_SNIPPET_CHARS = 220;                   // keep tooltips compact
+  const cache = new Map();                         // href -> { html, title, className, module, snippet }
+
+  let tooltipEl = null;
+  let hideTimer = null;
+  let showTimer = null;
+
+  function createTooltip() {
+    if (tooltipEl) return tooltipEl;
+    tooltipEl = document.createElement('div');
+    tooltipEl.className = 'agda-tooltip hidden';
+    tooltipEl.setAttribute('role', 'tooltip');
+    tooltipEl.innerHTML = '
';
+    document.body.appendChild(tooltipEl);
+    return tooltipEl;
+  }
+
+  function positionTooltip(evt, el) {
+    const pad = 12;
+    const vw = window.innerWidth;
+    const vh = window.innerHeight;
+    const rect = el.getBoundingClientRect();
+    const tipRect = tooltipEl.getBoundingClientRect();
+    let top = rect.bottom + window.scrollY + pad;
+    let left = evt.clientX + window.scrollX + pad;
+
+    // if overflowing right edge, shift left
+    if (left + tipRect.width > window.scrollX + vw - pad) {
+      left = Math.max(window.scrollX + pad, vw + window.scrollX - tipRect.width - pad);
+    }
+    // if too low, pop above
+    if (top + tipRect.height > window.scrollY + vh - pad) {
+      top = rect.top + window.scrollY - tipRect.height - pad;
+    }
+    tooltipEl.style.top = `${top}px`;
+    tooltipEl.style.left = `${left}px`;
+  }
+
+  function sanitize(text) {
+    // very small helper: we only ever insert our own strings; still, be safe
+    const div = document.createElement('div');
+    div.textContent = text == null ? '' : String(text);
+    return div.innerHTML;
+  }
+
+  function inferTokenInfo(a) {
+    // Try to infer token info from the Agda link classes + URL
+    const classes = (a.getAttribute('class') || '').split(/\s+/).filter(Boolean);
+    const agdaClass = classes.find(c => /^(Function|Field|Datatype|Record|Module|Primitive|InductiveConstructor|Operator)$/.test(c)) || 'Symbol';
+    const href = a.getAttribute('href') || '';
+    const url = new URL(href, window.location.href);
+    const moduleFile = (url.pathname.split('/').pop() || '').replace(/\.html$/,'');
+    const moduleName = moduleFile || 'Module';
+    // The visible label (basename) is often adjacent; fall back to text
+    const basename = a.textContent.trim() || moduleName;
+    const anchor = url.hash ? url.hash.slice(1) : '';
+    return { href: url.href, basename, agdaClass, moduleName, anchor };
+  }
+
+  async function fetchSnippet(href, anchor) {
+    try {
+      const res = await fetch(href, { credentials: 'same-origin' });
+      if (!res.ok) throw new Error(`HTTP ${res.status}`);
+      const html = await res.text();
+
+      const dom = new DOMParser().parseFromString(html, 'text/html');
+
+      // 1) Find the anchor element, then its closest Agda 
+      const target = anchor ? dom.getElementById(anchor) : null;
+      const pre = target ? target.closest('pre.Agda') : dom.querySelector('pre.Agda');
+      if (!pre) return { snippet: '' };
+
+      // 2) Compute the anchor's character offset within that 
+      const index = target ? charIndexWithin(pre, target) : -1;
+
+      // 3) Extract a multi-line definition block that surrounds the anchor
+      const text = pre.textContent || '';
+      const { block } = extractDefinitionBlock(text, index, {
+        // -- tweakable knobs --
+        minLines: 2,     // default: 2 lines
+        maxLines: 14,    // default: 14 lines
+        maxChars: 1200,  // hard cap to keep tooltips snappy
+        includeUpwardSignature: true,
+      });
+
+      return { snippet: block.trim() };
+    } catch (_e) {
+      return { snippet: '' };
+    }
+  }
+  // async function fetchSnippet(href, anchor) {
+  //   try {
+  //     const res = await fetch(href, { credentials: 'same-origin' });
+  //     if (!res.ok) throw new Error(`HTTP ${res.status}`);
+  //     const html = await res.text();
+
+  //     // Best-effort: parse the target page & grab nearby code around the anchor
+  //     const dom = new DOMParser().parseFromString(html, 'text/html');
+  //     const target = anchor ? dom.getElementById(anchor) : null;
+  //     const pre = target ? target.closest('pre.Agda') : dom.querySelector('pre.Agda');
+
+  //     if (!pre) return { snippet: '' };
+
+  //     // Convert the 
 to text and extract a compact snippet around the anchor id
+  //     const preText = pre.textContent || '';
+  //     if (!preText) return { snippet: '' };
+
+  //     let snippet = preText;
+  //     // Try to bias toward the area containing the anchor id text (Agda puts ids on , not text;
+  //     // so we approximate by taking the middle of the 
 if we don't find anything)
+  //     const mid = Math.floor(preText.length / 2);
+  //     const start = Math.max(0, mid - Math.floor(MAX_SNIPPET_CHARS / 2));
+  //     snippet = preText.slice(start, start + MAX_SNIPPET_CHARS).trim();
+
+  //     // Normalize whitespace; keep “code” flavor
+  //     snippet = snippet.replace(/\s+\n/g, '\n').replace(/\n{3,}/g, '\n\n');
+
+  //     return { snippet };
+  //   } catch (_e) {
+  //     return { snippet: '' };
+  //   }
+  // }
+
+  /**
+   * Compute the character index of `node` relative to the start of `root`,
+   * by using a DOM Range. Falls back to -1 if anything fails.
+   */
+  function charIndexWithin(root, node) {
+    try {
+      const r = document.createRange();
+      r.setStart(root, 0);
+      r.setEnd(node, 0);
+      return r.toString().length;
+    } catch {
+      return -1;
+    }
+  }
+
+  /**
+   * Heuristically extract a "definition block" around `anchorIndex`.
+   * Strategy:
+   *  - Split 
 text into lines, track cumulative offsets.
+   *  - Find the line containing anchorIndex (or mid if -1).
+   *  - Expand upward to include header/signature lines:
+   *      - previous non-empty lines that are less-indented than the current line (headers),
+   *      - or that look like a type signature (contains ':' or 'record'/'data'/'module').
+   *  - Expand downward while:
+   *      - line is indented >= firstDefIndent (continuation/clauses),
+   *      - OR it’s a clause/where/with line,
+   *      - stop at first blank line following content.
+   *  - Enforce min/max lines and maxChars guardrails.
+   */
+  function extractDefinitionBlock(text, anchorIndex, opts) {
+    const {
+      minLines = 2,
+      maxLines = 12,
+      maxChars = 1000,
+      includeUpwardSignature = true,
+    } = opts || {};
+
+    const lines = text.split(/\r?\n/);
+    const lens = lines.map(l => l.length + 1); // +1 for newline
+    const starts = new Array(lines.length);
+    let acc = 0;
+    for (let i = 0; i < lines.length; i++) {
+      starts[i] = acc;
+      acc += lens[i];
+    }
+
+    // Find anchor line (or fallback to middle line)
+    let iAnchor = 0;
+    if (anchorIndex >= 0) {
+      for (let i = 0; i < starts.length; i++) {
+        const s = starts[i];
+        const e = s + Math.max(0, lens[i] - 1); // exclude trailing newline
+        if (anchorIndex >= s && anchorIndex <= e) { iAnchor = i; break; }
+        if (anchorIndex < s) { iAnchor = Math.max(0, i - 1); break; }
+        if (i === starts.length - 1) iAnchor = i;
+      }
+    } else {
+      iAnchor = Math.floor(lines.length / 2);
+    }
+
+    // Helpers
+    const indent = l => (l.match(/^\s*/)?.[0]?.length ?? 0);
+    const isBlank = l => /^\s*$/.test(l);
+    const looksLikeHeader = l =>
+      /\brecord\b|\bdata\b|\bmodule\b|\bconstructor\b/.test(l) || /:/.test(l);
+    const looksLikeClause = l =>
+      /\bwhere\b|\bwith\b|^\s*\|/.test(l) || /:=|=\s*$|→|→\s*$/.test(l);
+
+    // 1) Seed line: the one with anchor
+    let start = iAnchor, end = iAnchor;
+
+    // 2) Expand upward for headers/signatures (optional)
+    if (includeUpwardSignature) {
+      let i = iAnchor - 1;
+      while (i >= 0) {
+        const l = lines[i];
+        if (isBlank(l)) { i--; continue; }
+        if (looksLikeHeader(l) || indent(l) <= indent(lines[start])) {
+          start = i; i--;
+        } else {
+          break;
+        }
+        if (end - start + 1 >= maxLines) break;
+      }
+    }
+
+    // 3) Expand downward for continuation/clauses
+    const firstIndent = indent(lines[start]);
+    let sawContent = false;
+    for (let i = end + 1; i < lines.length; i++) {
+      const l = lines[i];
+      if (isBlank(l)) {
+        if (sawContent) { end = i - 1; break; }
+        // if blank before any content, skip it but don't count it
+        continue;
+      }
+      const ind = indent(l);
+      if (ind >= firstIndent || looksLikeClause(l)) {
+        end = i;
+        sawContent = true;
+      } else {
+        // hit a new top-level thing
+        break;
+      }
+      if (end - start + 1 >= maxLines) break;
+    }
+
+    // 4) Ensure at least minLines (extend down a bit if needed)
+    while (end - start + 1 < minLines && end + 1 < lines.length && !isBlank(lines[end + 1])) {
+      end++;
+    }
+
+    // 5) Compose block + enforce maxChars (trim softly on line boundary)
+    let blockLines = lines.slice(start, end + 1);
+    let block = blockLines.join('\n');
+    if (block.length > maxChars) {
+      // trim to nearest earlier newline before maxChars
+      const cut = block.lastIndexOf('\n', maxChars);
+      block = block.slice(0, cut > 0 ? cut : maxChars) + '\n…';
+    }
+
+    return { block, start, end, iAnchor };
+  }
+
+
+
+  function renderTooltipContent(info, snippet) {
+    const { href, basename, agdaClass, moduleName } = info;
+    const header = `

+        ${sanitize(agdaClass)}
+        ${sanitize(basename)}
+        · ${sanitize(moduleName)}
+      
`;
+
+    const body = snippet
+      ? `
${sanitize(snippet)}
`
+      : `
No preview available.
`;
+
+    const footer = `

+        Open definition ↗
+      
`;
+
+    return header + body + footer;
+  }
+
+  function showTooltip(evt, a, content) {
+    const el = createTooltip();
+    el.querySelector('.agda-tooltip-inner').innerHTML = content;
+    el.classList.remove('hidden');
+    positionTooltip(evt, a);
+  }
+
+  function hideTooltipSoon() {
+    if (!tooltipEl) return;
+    tooltipEl.classList.add('hidden');
+  }
+
+  async function handleEnter(evt) {
+    const a = evt.currentTarget;
+    clearTimeout(hideTimer);
+    clearTimeout(showTimer);
+
+    showTimer = setTimeout(async () => {
+      const key = a.href;
+      let data = cache.get(key);
+
+      const info = inferTokenInfo(a);
+      if (!data) {
+        // Render a fast “skeleton” immediately
+        const skeleton = renderTooltipContent(info, '');
+        showTooltip(evt, a, skeleton);
+
+        // Fetch snippet (once)
+        const { snippet } = await fetchSnippet(info.href, info.anchor);
+        data = { info, snippet };
+        cache.set(key, data);
+      }
+
+      const html = renderTooltipContent(info, data.snippet);
+      showTooltip(evt, a, html);
+    }, HOVER_DELAY_MS);
+  }
+
+  function handleLeave() {
+    clearTimeout(showTimer);
+    hideTimer = setTimeout(hideTooltipSoon, 60);
+  }
+
+  function handleMove(evt) {
+    if (!tooltipEl || tooltipEl.classList.contains('hidden')) return;
+    const a = evt.currentTarget;
+    positionTooltip(evt, a);
+  }
+
+  function wireUp() {
+    const anchors = document.querySelectorAll(HOVER_SELECTOR);
+    anchors.forEach(a => {
+      // Skip non-HTTP links
+      const href = a.getAttribute('href');
+      if (!href || href.startsWith('#') || href.startsWith('mailto:')) return;
+
+      a.addEventListener('mouseenter', handleEnter, { passive: true });
+      a.addEventListener('mouseleave', handleLeave, { passive: true });
+      a.addEventListener('mousemove', handleMove,   { passive: true });
+    });
+
+    // Keep tooltip from flickering if user hovers the tooltip itself
+    createTooltip();
+    tooltipEl.addEventListener('mouseenter', () => clearTimeout(hideTimer));
+    tooltipEl.addEventListener('mouseleave', hideTooltipSoon);
+  }
+
+  if (document.readyState === 'loading') {
+    document.addEventListener('DOMContentLoaded', wireUp);
+  } else {
+    wireUp();
+  }
+})();
diff --git a/build-tools/static/md/mkdocs/mkdocs.yml b/build-tools/static/md/mkdocs/mkdocs.yml
index e4331f2d3..bd0967a61 100644
--- a/build-tools/static/md/mkdocs/mkdocs.yml
+++ b/build-tools/static/md/mkdocs/mkdocs.yml
@@ -71,6 +71,7 @@ extra_css:
   # auto-generated by Agda fls backend (load after katex.css)
   # - css/Agda.css
   - css/custom.css
+  - css/agda-hover.css
 
 extra_javascript:
   # KaTeX JavaScript
@@ -82,6 +83,7 @@ extra_javascript:
   - AgdaKaTeX.js
   - https://cdn.jsdelivr.net/npm/chart.js
   - js/custom.js
+  - js/agda-hover.js
 
 markdown_extensions:
   - admonition                # call-out boxes like !!! note

From d5591afc0256069aec9813d1abbeadafae5792a0 Mon Sep 17 00:00:00 2001
From: William DeMeo 
Date: Fri, 10 Oct 2025 00:17:29 -0600
Subject: [PATCH 2/2] second pass

---
 .../static/md/mkdocs/docs/css/agda-hover.css  | 210 +++++++++---------
 .../static/md/mkdocs/docs/js/agda-hover.js    |  13 +-
 2 files changed, 103 insertions(+), 120 deletions(-)

diff --git a/build-tools/static/md/mkdocs/docs/css/agda-hover.css b/build-tools/static/md/mkdocs/docs/css/agda-hover.css
index 5308751dd..6a741fad7 100644
--- a/build-tools/static/md/mkdocs/docs/css/agda-hover.css
+++ b/build-tools/static/md/mkdocs/docs/css/agda-hover.css
@@ -1,146 +1,134 @@
-/* === Agda hover tooltip ================================================== */
+/* ==========================================================================
+   Agda Hover Tooltip (clean + compact)
+   --------------------------------------------------------------------------
+   Tuning knobs:
+   - --agda-font-base: base font size used for most text in the tooltip
+   - --agda-font-code: font size for code snippet
+   - --agda-line-base: line-height for body text
+   - --agda-line-code: line-height for code snippet
+   - --agda-width:     max width of the tooltip
+   - --agda-ch:        max code line width in characters (for readability)
+   ========================================================================== */
+
+/* === Theme + size tokens ================================================= */
+:root,
+[data-md-color-scheme="default"] {
+  /* Sizes (make smaller/larger here) */
+  --agda-font-base: 0.72rem;   /* overall base text size (very compact) */
+  --agda-font-code: 0.70rem;   /* code size (very compact) */
+  --agda-line-base: 1.05rem;   /* base line-height */
+  --agda-line-code: 1.06rem;   /* code line-height */
+  --agda-width:     min(34rem, 90vw); /* tooltip max width */
+  --agda-ch:        68ch;      /* max code line width */
+
+  /* Colors (light) */
+  --agda-tip-bg:     #ffffff;
+  --agda-tip-fg:     #1f2328;
+  --agda-tip-border: rgba(0,0,0,.10);
+  --agda-tip-link:   #0969da;  /* reserved if links added later */
+  --agda-tip-codebg: rgba(127,127,127,.06);
+  --agda-shadow:     0 6px 16px rgba(0,0,0,.14), 0 2px 6px rgba(0,0,0,.10);
+}
+
+[data-md-color-scheme="slate"] {
+  /* Colors (dark) */
+  --agda-tip-bg:     #1f2430;
+  --agda-tip-fg:     #f4f6f8;
+  --agda-tip-border: rgba(255,255,255,.14);
+  --agda-tip-link:   #8ab4ff;
+  --agda-tip-codebg: rgba(255,255,255,.04);
+  --agda-shadow:     0 6px 16px rgba(0,0,0,.25), 0 2px 6px rgba(0,0,0,.18);
+}
+
+/* === Tooltip container =================================================== */
 .agda-tooltip {
   position: absolute;
   z-index: 2000;
-  max-width: min(42rem, 92vw);
-  box-shadow: 0 10px 26px rgba(0,0,0,.18), 0 4px 10px rgba(0,0,0,.12);
-  border-radius: .5rem;
-  border: 1px solid rgba(0,0,0,.1);
-  backdrop-filter: blur(6px);
-  -webkit-backdrop-filter: blur(6px);
-  transition: opacity .12s ease, transform .12s ease;
-  transform: translateY(-2px);
+  max-width: var(--agda-width);
+  background: var(--agda-tip-bg);
+  color: var(--agda-tip-fg);
+  border: 1px solid var(--agda-tip-border);
+  border-radius: .35rem;
+  box-shadow: var(--agda-shadow);
   opacity: 1;
+  transform: none;
+
+  /* Hover-only behavior: no interactions inside the box */
+  pointer-events: none;
+  /* To allow selection/copy, flip to 'auto' */
+}
+
+.agda-tooltip.hidden {
+  opacity: 0;
+  /* Tooltip is purely informational; hide by opacity. */
+  /* (JS is already preventing pointer events when hidden.) */
 }
-.agda-tooltip.hidden { opacity: 0; pointer-events: none; }
 
+/* === Inner layout ======================================================== */
 .agda-tooltip .agda-tooltip-inner {
-  padding: .75rem .9rem .7rem .9rem;
-  font-size: .92rem;
-  line-height: 1.25rem;
+  padding: .36rem .48rem;   /* very tight padding */
+  font-size: var(--agda-font-base);
+  line-height: var(--agda-line-base);
 }
 
+/* === Header line (kind · name · module) ================================= */
 .agda-tip-head {
   display: flex;
   align-items: baseline;
-  gap: .5rem;
-  margin-bottom: .4rem;
+  gap: .32rem;
+  margin-bottom: .16rem;
   font-weight: 600;
 }
 
 .agda-kind {
-  font-size: .78rem;
+  font-size: calc(var(--agda-font-base) - 0.06rem); /* tiny label */
+  letter-spacing: .04em;
   text-transform: uppercase;
-  letter-spacing: .06em;
-  opacity: .8;
+  opacity: .72;
 }
 
 .agda-name {
-  font-family: ui-monospace, SFMono-Regular, Menlo, Monaco, Consolas, "Liberation Mono", "Courier New", monospace;
+  font-family: ui-monospace, SFMono-Regular, Menlo, Monaco, Consolas,
+               "Liberation Mono", "Courier New", monospace;
+  font-size: calc(var(--agda-font-base) - 0.02rem);
   font-weight: 700;
 }
 
 .agda-module {
   margin-left: auto;
-  font-size: .78rem;
-  opacity: .7;
+  font-size: calc(var(--agda-font-base) - 0.08rem);
+  opacity: .55;
 }
 
+/* === Code preview ======================================================== */
 .agda-tip-snippet {
-  white-space: pre-wrap;
-  margin: .25rem 0 .5rem 0;
-  padding: .5rem .6rem;
-  border-radius: .4rem;
-  background: rgba(127,127,127,.08);
-  font-size: .85rem;
-  overflow: hidden;
-}
-
-.agda-tip-empty {
-  margin: .25rem 0 .5rem 0;
-  font-size: .85rem;
-  opacity: .85;
-}
-
-.agda-tip-actions {
-  display: flex;
-  justify-content: flex-end;
-}
-.agda-open-def {
-  text-decoration: none;
-  font-weight: 600;
-}
-
-/* Light/dark theming with MkDocs Material */
-:root,
-[data-md-color-scheme="default"] {
-  --agda-tip-bg: #ffffff;
-  --agda-tip-fg: #1f2328;
-  --agda-tip-link: #0969da;
-  --agda-tip-border: rgba(0,0,0,.1);
-}
-[data-md-color-scheme="slate"] {
-  --agda-tip-bg: #1f2430;
-  --agda-tip-fg: #f4f6f8;
-  --agda-tip-link: #8ab4ff;
-  --agda-tip-border: rgba(255,255,255,.14);
-  .agda-tip-snippet { background: rgba(255,255,255,.06); }
-}
-
-.agda-tooltip {
-  background: var(--agda-tip-bg);
-  color: var(--agda-tip-fg);
-  border-color: var(--agda-tip-border);
-}
-.agda-open-def { color: var(--agda-tip-link); }
-/* === Agda tooltip polish (compact & clean) =============================== */
-.agda-tooltip .agda-tooltip-inner {
-  padding: .55rem .7rem .55rem .7rem;
-  font-size: .88rem;              /* smaller base */
-  line-height: 1.2rem;
-}
-
-.agda-tip-head {
-  gap: .4rem;
-  margin-bottom: .25rem;
-  font-weight: 600;
-}
+  margin: .10rem 0 0 0;
+  padding: .30rem .40rem;
+  border-radius: .28rem;
+  background: var(--agda-tip-codebg);
 
-.agda-kind {
-  font-size: .72rem;
-  letter-spacing: .05em;
-  opacity: .75;
-}
+  font-family: ui-monospace, SFMono-Regular, Menlo, Monaco, Consolas,
+               "Liberation Mono", "Courier New", monospace;
+  font-size: var(--agda-font-code);
+  line-height: var(--agda-line-code);
 
-.agda-name {
-  font-size: .9rem;               /* tighter monospace name */
-  font-weight: 700;
-}
-
-.agda-module {
-  font-size: .72rem;
-  opacity: .6;
-}
+  /* Keep Agda formatting exactly. If you prefer wrapping, change to 'pre-wrap'. */
+  white-space: pre;
 
-.agda-tip-snippet {
-  margin: .2rem 0 .4rem 0;
-  padding: .45rem .55rem;
-  border-radius: .35rem;
-  font-size: .82rem;              /* smaller code */
-  line-height: 1.15rem;
-  max-width: 80ch;                /* avoid ultra-wide lines */
-  overflow-x: auto;               /* allow horizontal scroll if needed */
-  white-space: pre;               /* preserve formatting exactly */
+  /* Width hygiene */
+  max-width: var(--agda-ch);
+  overflow-x: auto;  /* allow horizontal scroll for long types */
+  overflow-y: hidden;
 }
 
-.agda-tooltip {
-  max-width: min(46rem, 92vw);    /* a bit narrower overall */
-  border-radius: .45rem;
-  box-shadow: 0 10px 22px rgba(0,0,0,.16), 0 3px 8px rgba(0,0,0,.10);
-  transform: translateY(-1px);
+/* When no snippet could be extracted */
+.agda-tip-empty {
+  margin: .12rem 0 0 0;
+  font-size: calc(var(--agda-font-base) - 0.04rem);
+  opacity: .85;
 }
 
-/* Dark mode nuance */
-[data-md-color-scheme="slate"] .agda-tip-snippet {
-  background: rgba(255,255,255,.04);
-}
+/* === Legacy / unused bits (kept inert) ================================== */
+/* If older CSS defines these, keep them invisible to avoid layout churn. */
+.agda-tip-actions { display: none !important; }
+.agda-open-def    { display: none !important; }
diff --git a/build-tools/static/md/mkdocs/docs/js/agda-hover.js b/build-tools/static/md/mkdocs/docs/js/agda-hover.js
index 8a13cb743..41e74d2c5 100644
--- a/build-tools/static/md/mkdocs/docs/js/agda-hover.js
+++ b/build-tools/static/md/mkdocs/docs/js/agda-hover.js
@@ -1,5 +1,5 @@
 // === Agda hover definitions ===============================================
-// Works on Agda-generated HTML embedded in your Markdown, i.e., inside 
.
+// Works on Agda-generated HTML embedded in Markdown, i.e., inside 
.
 // Shows a tooltip on hover with (1) token info, (2) link to full definition,
 // and (best-effort) a short snippet from the target page near the anchor.
 
@@ -253,10 +253,9 @@
     return { block, start, end, iAnchor };
   }
 
-
-
   function renderTooltipContent(info, snippet) {
-    const { href, basename, agdaClass, moduleName } = info;
+    const { basename, agdaClass, moduleName } = info;
+
     const header = `

         ${sanitize(agdaClass)}
         ${sanitize(basename)}
@@ -267,11 +266,7 @@
       ? `
${sanitize(snippet)}
`
       : `
No preview available.
`;
 
-    const footer = `

-        Open definition ↗
-      
`;
-
-    return header + body + footer;
+    return header + body;  // ⟵ no footer
   }
 
   function showTooltip(evt, a, content) {