esp-hal/resources/select.html.jinja
Jesse Braham 15f2e914d6
Patch generated documentation to include a version selector (#3131)
* Refactor all documentation-related functions into their own module

* Rename `Package::should_document` to `Package::is_published`

* Patch the generated documentation to include a version selector

* Only try to fetch package manifest if `deploy-docs` feature is enabled
2025-02-13 08:33:25 +00:00

49 lines
1.5 KiB
Django/Jinja

<div style="margin-top: 0.5rem; width: 100%">
<label for="version-select">Version:</label>
<select id="version-select" name="version-select" style="text-align: center; width: 100%">
<option value="{{ version }}" selected="selected">{{ version }}</option>
</select>
</div>
<script type="text/javascript">
const select = document.querySelector("#version-select");
select.addEventListener("change", (e) => {
const selected = select.value;
// Replace the existing version number in the URL with the newly
// selected version:
let href = window.location.href;
href = href.replace(/[\d]+\.[\d]+\.[\d]+[^\/]*/g, selected);
// Redirect to the new URL:
window.location.href = href;
});
document.addEventListener("DOMContentLoaded", (e) => {
const selected = select.value;
// Remove any options currently present in the select box:
for (let child of select.children) {
child.remove();
}
// Load the manifest JSON file and re-populate the select box with new
// options for all available versions:
const manifestUrl = "{{ base_url }}/{{ package }}/manifest.json";
fetch(manifestUrl)
.then((res) => res.json())
.then(({ versions }) => {
for (let version of versions) {
let option = document.createElement("option");
option.text = version;
option.value = version;
select.appendChild(option);
}
select.value = selected;
})
.catch((err) => console.error(err));
});
</script>