Testing of the @doc-json output
fix(odoc-docsite): inject extension CSS/JS on SPA navigation
The docsite shell's navigateTo() function fetches new pages and replaces
content, but discarded <head> elements from the fetched page. Extension
resources like admonition.css were never loaded during client-side
navigation, only on full page loads.
Scan the fetched page's <head> for stylesheet and script elements,
resolve their URLs, and append any missing ones to the live document.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
+24
+24
src/odoc_docsite_js.ml
+24
src/odoc_docsite_js.ml
···
311
311
document.title = newTitle.textContent;
312
312
}
313
313
314
+
// Inject extension CSS/JS from the fetched page that aren't already loaded
315
+
var fetchedPageBase = ROOT_URL + url;
316
+
doc.querySelectorAll('head link[rel="stylesheet"], head script[src]').forEach(function(el) {
317
+
var attr = el.tagName === 'LINK' ? 'href' : 'src';
318
+
var resUrl = el.getAttribute(attr);
319
+
if (!resUrl) return;
320
+
// Resolve to absolute for comparison
321
+
var abs = new URL(resUrl, fetchedPageBase).href;
322
+
var selector = el.tagName === 'LINK'
323
+
? 'link[rel="stylesheet"]'
324
+
: 'script[src]';
325
+
var already = Array.from(document.querySelectorAll('head ' + selector)).some(function(existing) {
326
+
var existingUrl = existing.getAttribute(attr);
327
+
if (!existingUrl) return false;
328
+
return new URL(existingUrl, window.location.href).href === abs;
329
+
});
330
+
if (!already) {
331
+
var clone = el.cloneNode(true);
332
+
// Fix relative URL to be root-relative
333
+
clone.setAttribute(attr, abs);
334
+
document.head.appendChild(clone);
335
+
}
336
+
});
337
+
314
338
CURRENT_URL = url;
315
339
if (pushState) {
316
340
history.pushState({ url: url }, '', ROOT_URL + url);