Merge pull request 'Fix #282: jumpnav visible on mobile initial load' (#285) from fix-282 into dev

The initial refresh() ran before the mobile layout settled (media queries,
fonts, async highlighting) and under-measured the content, leaving #jumpnav
hidden on long pastes at 375x812 until a resize event. Re-check after a
double rAF, on window load, after 300ms, and via a ResizeObserver on
document.body for late content growth. Editor textarea scroller unchanged.

internal/web/static/jump.js

@@ -38,4 +38,14 @@
   window.addEventListener('resize', refresh);
   if (scroller !== window && scroller) scroller.addEventListener('input', refresh);
   refresh();
+  /* #282: the first evaluation can run before the layout settles (media
+     queries, web fonts, async highlighting) and under-measure the content,
+     leaving the nav hidden on long pages. Re-check once a real layout exists
+     and after load; the ResizeObserver also catches late content growth. */
+  requestAnimationFrame(function () { requestAnimationFrame(refresh); });
+  window.addEventListener('load', refresh);
+  window.setTimeout(refresh, 300);
+  if (window.ResizeObserver && scroller === window && document.body) {
+    new ResizeObserver(refresh).observe(document.body);
+  }
 })();