Michael Rabinovich Cursor commited on
Commit ·
f07f508
1
Parent(s): 4090e8a
leaderboard: metrics tab single-scroll + polish on mobile
Browse filesOn phones the Metrics tab's fixed 85vh iframe made a nested scroll-box.
Auto-size the embedding iframe to the page content on narrow screens so
it's a single page scroll (desktop keeps its fixed height, which reads
well). In-page anchor links use scrollIntoView so they still work when
the iframe has no internal scroll. Also tighten padding/formula/table
sizing and shrink the vh end-spacer on mobile.
Co-authored-by: Cursor <cursoragent@cursor.com>
- metrics_page.py +47 -0
metrics_page.py
CHANGED
|
@@ -111,6 +111,20 @@ figure.fig figcaption { font-size: 0.84em; color: #5b6170; margin-top: 6px;
|
|
| 111 |
max-width: 560px; }
|
| 112 |
.weight-pill { font-family: monospace; font-size: 0.8em; padding: 1px 7px;
|
| 113 |
border-radius: 6px; background: #eceff1; color: #37474f; }
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 114 |
"""
|
| 115 |
|
| 116 |
|
|
@@ -355,5 +369,38 @@ def build_metrics_page() -> str:
|
|
| 355 |
"one.</p>"
|
| 356 |
f"{toc}{overview}{validity}{shape}{topology}{interface}{editing}"
|
| 357 |
f"{footer}"
|
|
|
|
| 358 |
"</body></html>"
|
| 359 |
)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 111 |
max-width: 560px; }
|
| 112 |
.weight-pill { font-family: monospace; font-size: 0.8em; padding: 1px 7px;
|
| 113 |
border-radius: 6px; background: #eceff1; color: #37474f; }
|
| 114 |
+
@media (max-width: 760px) {
|
| 115 |
+
/* On phones the page flows in a single scroll (the embedding iframe is
|
| 116 |
+
auto-sized to content, see the inline script), so the big vh end-spacer
|
| 117 |
+
would add a screenful of blank -- shrink it to a fixed nub. Tighten the
|
| 118 |
+
reading frame a touch too. */
|
| 119 |
+
body { padding: 16px 14px 28px; }
|
| 120 |
+
h1 { font-size: 1.5em; }
|
| 121 |
+
.card { padding: 16px 16px; }
|
| 122 |
+
.card h2 { font-size: 1.12em; }
|
| 123 |
+
pre.formula { font-size: 0.78em; padding: 12px 13px; }
|
| 124 |
+
table { font-size: 0.86em; }
|
| 125 |
+
th, td { padding: 6px 8px; }
|
| 126 |
+
.endspace { height: 24px; }
|
| 127 |
+
}
|
| 128 |
"""
|
| 129 |
|
| 130 |
|
|
|
|
| 369 |
"one.</p>"
|
| 370 |
f"{toc}{overview}{validity}{shape}{topology}{interface}{editing}"
|
| 371 |
f"{footer}"
|
| 372 |
+
f"<script>{_JS}</script>"
|
| 373 |
"</body></html>"
|
| 374 |
)
|
| 375 |
+
|
| 376 |
+
|
| 377 |
+
# On phones, size the embedding iframe to the page's content so the Metrics tab
|
| 378 |
+
# is a single page scroll instead of a nested 85vh scroll-box (the desktop tab
|
| 379 |
+
# keeps its fixed height -- it reads well there). In-page anchor links use
|
| 380 |
+
# scrollIntoView so they still work when the iframe has no internal scroll (it
|
| 381 |
+
# walks up to scroll the parent frame); on the standalone /metrics route there
|
| 382 |
+
# is no frame and the browser just scrolls normally. All wrapped in try/catch:
|
| 383 |
+
# frameElement/parent access is fine for this same-origin iframe but must never
|
| 384 |
+
# throw if that ever changes.
|
| 385 |
+
_JS = """
|
| 386 |
+
(function () {
|
| 387 |
+
var narrow = (window.innerWidth || 1000) < 760;
|
| 388 |
+
function fit() {
|
| 389 |
+
if (!narrow) return;
|
| 390 |
+
try {
|
| 391 |
+
var fe = window.frameElement;
|
| 392 |
+
if (fe) fe.style.height = Math.ceil(document.documentElement.scrollHeight) + 'px';
|
| 393 |
+
} catch (e) { /* keep the CSS fallback height */ }
|
| 394 |
+
}
|
| 395 |
+
document.addEventListener('click', function (e) {
|
| 396 |
+
var a = e.target && e.target.closest ? e.target.closest('a[href^="#"]') : null;
|
| 397 |
+
if (!a) return;
|
| 398 |
+
var el = document.getElementById(a.getAttribute('href').slice(1));
|
| 399 |
+
if (el) { e.preventDefault(); el.scrollIntoView({ behavior: 'smooth', block: 'start' }); }
|
| 400 |
+
});
|
| 401 |
+
window.addEventListener('load', fit);
|
| 402 |
+
window.addEventListener('resize', function () { narrow = (window.innerWidth || 1000) < 760; fit(); });
|
| 403 |
+
if (window.ResizeObserver) { try { new ResizeObserver(fit).observe(document.body); } catch (e) {} }
|
| 404 |
+
fit();
|
| 405 |
+
})();
|
| 406 |
+
"""
|