A graphviz extension for odoc
Add odoc-spa-loaded event for extension SPA support
The SPA shell now dispatches a 'odoc-spa-loaded' custom event on
document after all external scripts from the fetched page have
loaded and inline scripts have executed. Extensions listen for
this event instead of polling for CDN library availability.
This replaces the unreliable polling approach — the MutationObserver
fires before CDN scripts load, and no further mutations occur to
trigger re-rendering. The custom event fires at exactly the right
moment: after content is swapped AND all scripts are ready.
Updated mermaid, dot, and msc extensions to use the new event.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
+9
-30
+9
-30
src/dot_extension.ml
+9
-30
src/dot_extension.ml
···
145
145
});
146
146
}
147
147
148
-
function init() {
149
-
renderAll();
150
-
observe();
151
-
if (typeof Viz === 'undefined' &&
152
-
document.querySelectorAll('.odoc-dot-diagram:not([data-dot-init])').length > 0) {
153
-
waitForViz();
154
-
}
155
-
}
156
-
157
148
if (document.readyState === 'loading') {
158
-
document.addEventListener('DOMContentLoaded', init);
149
+
document.addEventListener('DOMContentLoaded', function() {
150
+
renderAll();
151
+
observe();
152
+
});
159
153
} else {
160
-
init();
154
+
renderAll();
155
+
observe();
161
156
}
162
157
163
158
function observe() {
164
-
new MutationObserver(function() {
165
-
renderAll();
166
-
if (typeof Viz === 'undefined' &&
167
-
document.querySelectorAll('.odoc-dot-diagram:not([data-dot-init])').length > 0) {
168
-
waitForViz();
169
-
}
170
-
}).observe(document.body, { childList: true, subtree: true });
171
-
}
172
-
173
-
var waitTimer = null;
174
-
function waitForViz() {
175
-
if (waitTimer) return;
176
-
waitTimer = setInterval(function() {
177
-
if (typeof Viz !== 'undefined') {
178
-
clearInterval(waitTimer);
179
-
waitTimer = null;
180
-
renderAll();
181
-
}
182
-
}, 200);
159
+
new MutationObserver(function() { renderAll(); })
160
+
.observe(document.body, { childList: true, subtree: true });
161
+
document.addEventListener('odoc-spa-loaded', function() { renderAll(); });
183
162
}
184
163
})();
185
164
|}