Skip to content

Commit 32869b3

Browse files
Deploying to main from @ amaranth-lang/amaranth@53d88ad 🚀
1 parent b09b2ac commit 32869b3

37 files changed

+245
-100
lines changed

docs/amaranth/latest/_static/documentation_options.js

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
const DOCUMENTATION_OPTIONS = {
2-
VERSION: '0.6.0.dev108',
2+
VERSION: '0.6.0.dev109',
33
LANGUAGE: 'en',
44
COLLAPSE_INDEX: false,
55
BUILDER: 'html',
Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
document.addEventListener('DOMContentLoaded', () => {
2+
let contentRoot = new URL(
3+
document.documentElement.dataset.content_root ?? DOCUMENTATION_OPTIONS.URL_ROOT,
4+
window.location.href,
5+
);
6+
7+
function insertVersionSwitch(versions) {
8+
let versionElement = document.querySelector('.wy-side-nav-search > .version');
9+
if (!versionElement) return;
10+
11+
let root = document.createElement('div');
12+
root.innerHTML = `
13+
<div class="switch-menus">
14+
<div class="version-switch"><select></select></div>
15+
</div>
16+
`;
17+
18+
let switchMenus = root.firstElementChild;
19+
let versionSwitch = switchMenus.firstElementChild;
20+
let versionSwitchSelect = versionSwitch.firstElementChild;
21+
22+
let versionElementStyles = getComputedStyle(versionElement);
23+
let cssStyleSheet = new CSSStyleSheet();
24+
cssStyleSheet.replaceSync(String.raw`
25+
.wy-side-nav-search > div.switch-menus {
26+
margin-top: ${versionElementStyles.marginTop};
27+
margin-bottom: ${versionElementStyles.marginBottom};
28+
color: ${versionElementStyles.color};
29+
30+
div.version-switch {
31+
select {
32+
display: inline-block;
33+
margin-right: -2rem;
34+
padding-right: 2rem;
35+
text-align-last: center;
36+
background: none;
37+
border: none;
38+
border-radius: 0em;
39+
box-shadow: none;
40+
font-family: inherit;
41+
font-size: 1em;
42+
font-weight: normal;
43+
color: inherit;
44+
cursor: pointer;
45+
appearance: none;
46+
47+
&:hover, &:active, &:focus {
48+
background: rgba(255, 255, 255, .1);
49+
color: rgba(255, 255, 255, .5);
50+
}
51+
52+
option {
53+
color: black;
54+
}
55+
}
56+
57+
&:has(> select):after {
58+
display: inline-block;
59+
width: 1.5em;
60+
height: 100%;
61+
padding: .1em;
62+
content: "\f0d7";
63+
font-size: 1em;
64+
line-height: 1.2em;
65+
font-family: FontAwesome;
66+
text-align: center;
67+
pointer-events: none;
68+
box-sizing: border-box;
69+
}
70+
}
71+
}
72+
`);
73+
document.adoptedStyleSheets.push(cssStyleSheet);
74+
75+
let currentVersion = DOCUMENTATION_OPTIONS.VERSION;
76+
if (!versions.includes(currentVersion)) {
77+
versions = [
78+
{ name: currentVersion, root_url: contentRoot },
79+
...versions,
80+
];
81+
}
82+
83+
for (let { name, root_url: rootURL } of versions) {
84+
rootURL = new URL(rootURL, window.location.href);
85+
86+
let versionOptionElement = document.createElement('option');
87+
versionOptionElement.textContent = name;
88+
versionOptionElement.dataset.url = rootURL;
89+
90+
if (name === currentVersion) {
91+
versionOptionElement.selected = true;
92+
}
93+
94+
versionSwitchSelect.appendChild(versionOptionElement);
95+
}
96+
97+
versionSwitchSelect.addEventListener('change', (event) => {
98+
let option = event.target.selectedIndex;
99+
let item = event.target.options[option];
100+
window.location.href = item.dataset.url;
101+
});
102+
103+
versionElement.replaceWith(switchMenus);
104+
}
105+
106+
fetch(new URL('../versions.json', contentRoot)).then(async (response) => {
107+
if (response.status !== 200) return;
108+
let versions = await response.json();
109+
insertVersionSwitch(versions);
110+
});
111+
});

docs/amaranth/latest/changes.html

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />
55

66
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
7-
<title>Changelog &mdash; Amaranth language &amp; toolchain 0.6.0.dev108 documentation</title>
7+
<title>Changelog &mdash; Amaranth language &amp; toolchain 0.6.0.dev109 documentation</title>
88
<link rel="stylesheet" type="text/css" href="_static/pygments.css?v=b86133f3" />
99
<link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
1010
<link rel="stylesheet" type="text/css" href="_static/platformpicker.css" />
@@ -17,10 +17,11 @@
1717

1818
<script src="_static/jquery.js?v=5d32c60e"></script>
1919
<script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
20-
<script src="_static/documentation_options.js?v=3c567cdd"></script>
20+
<script src="_static/documentation_options.js?v=982ef8c4"></script>
2121
<script src="_static/doctools.js?v=9a2dae69"></script>
2222
<script src="_static/sphinx_highlight.js?v=dc90522c"></script>
2323
<script src="_static/platformpicker.js"></script>
24+
<script src="_static/version-switch.js?v=6c8574fb"></script>
2425
<script src="_static/js/theme.js"></script>
2526
<link rel="index" title="Index" href="genindex.html" />
2627
<link rel="search" title="Search" href="search.html" />
@@ -41,7 +42,7 @@
4142
<img src="_static/logo.png" class="logo" alt="Logo"/>
4243
</a>
4344
<div class="version">
44-
0.6.0.dev108
45+
0.6.0.dev109
4546
</div>
4647
<div role="search">
4748
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">

docs/amaranth/latest/conf.py

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@
5757
html_theme = "sphinx_rtd_theme"
5858
html_static_path = ["_static"]
5959
html_css_files = ["custom.css"]
60+
html_js_files = ["version-switch.js"]
6061
html_logo = "_static/logo.png"
6162

6263
rst_prolog = """

docs/amaranth/latest/contrib.html

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />
55

66
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
7-
<title>Contributing &mdash; Amaranth language &amp; toolchain 0.6.0.dev108 documentation</title>
7+
<title>Contributing &mdash; Amaranth language &amp; toolchain 0.6.0.dev109 documentation</title>
88
<link rel="stylesheet" type="text/css" href="_static/pygments.css?v=b86133f3" />
99
<link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
1010
<link rel="stylesheet" type="text/css" href="_static/platformpicker.css" />
@@ -17,10 +17,11 @@
1717

1818
<script src="_static/jquery.js?v=5d32c60e"></script>
1919
<script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
20-
<script src="_static/documentation_options.js?v=3c567cdd"></script>
20+
<script src="_static/documentation_options.js?v=982ef8c4"></script>
2121
<script src="_static/doctools.js?v=9a2dae69"></script>
2222
<script src="_static/sphinx_highlight.js?v=dc90522c"></script>
2323
<script src="_static/platformpicker.js"></script>
24+
<script src="_static/version-switch.js?v=6c8574fb"></script>
2425
<script src="_static/js/theme.js"></script>
2526
<link rel="index" title="Index" href="genindex.html" />
2627
<link rel="search" title="Search" href="search.html" />
@@ -40,7 +41,7 @@
4041
<img src="_static/logo.png" class="logo" alt="Logo"/>
4142
</a>
4243
<div class="version">
43-
0.6.0.dev108
44+
0.6.0.dev109
4445
</div>
4546
<div role="search">
4647
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">

docs/amaranth/latest/cover.html

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />
55

66
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
7-
<title>Amaranth project documentation &mdash; Amaranth language &amp; toolchain 0.6.0.dev108 documentation</title>
7+
<title>Amaranth project documentation &mdash; Amaranth language &amp; toolchain 0.6.0.dev109 documentation</title>
88
<link rel="stylesheet" type="text/css" href="_static/pygments.css?v=b86133f3" />
99
<link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
1010
<link rel="stylesheet" type="text/css" href="_static/platformpicker.css" />
@@ -17,10 +17,11 @@
1717

1818
<script src="_static/jquery.js?v=5d32c60e"></script>
1919
<script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
20-
<script src="_static/documentation_options.js?v=3c567cdd"></script>
20+
<script src="_static/documentation_options.js?v=982ef8c4"></script>
2121
<script src="_static/doctools.js?v=9a2dae69"></script>
2222
<script src="_static/sphinx_highlight.js?v=dc90522c"></script>
2323
<script src="_static/platformpicker.js"></script>
24+
<script src="_static/version-switch.js?v=6c8574fb"></script>
2425
<script src="_static/js/theme.js"></script>
2526
<link rel="index" title="Index" href="genindex.html" />
2627
<link rel="search" title="Search" href="search.html" />
@@ -40,7 +41,7 @@
4041
<img src="_static/logo.png" class="logo" alt="Logo"/>
4142
</a>
4243
<div class="version">
43-
0.6.0.dev108
44+
0.6.0.dev109
4445
</div>
4546
<div role="search">
4647
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">

docs/amaranth/latest/genindex.html

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
<head>
44
<meta charset="utf-8" />
55
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
6-
<title>Index &mdash; Amaranth language &amp; toolchain 0.6.0.dev108 documentation</title>
6+
<title>Index &mdash; Amaranth language &amp; toolchain 0.6.0.dev109 documentation</title>
77
<link rel="stylesheet" type="text/css" href="_static/pygments.css?v=b86133f3" />
88
<link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
99
<link rel="stylesheet" type="text/css" href="_static/platformpicker.css" />
@@ -16,10 +16,11 @@
1616

1717
<script src="_static/jquery.js?v=5d32c60e"></script>
1818
<script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
19-
<script src="_static/documentation_options.js?v=3c567cdd"></script>
19+
<script src="_static/documentation_options.js?v=982ef8c4"></script>
2020
<script src="_static/doctools.js?v=9a2dae69"></script>
2121
<script src="_static/sphinx_highlight.js?v=dc90522c"></script>
2222
<script src="_static/platformpicker.js"></script>
23+
<script src="_static/version-switch.js?v=6c8574fb"></script>
2324
<script src="_static/js/theme.js"></script>
2425
<link rel="index" title="Index" href="#" />
2526
<link rel="search" title="Search" href="search.html" />
@@ -38,7 +39,7 @@
3839
<img src="_static/logo.png" class="logo" alt="Logo"/>
3940
</a>
4041
<div class="version">
41-
0.6.0.dev108
42+
0.6.0.dev109
4243
</div>
4344
<div role="search">
4445
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">

docs/amaranth/latest/guide.html

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />
55

66
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
7-
<title>Language guide &mdash; Amaranth language &amp; toolchain 0.6.0.dev108 documentation</title>
7+
<title>Language guide &mdash; Amaranth language &amp; toolchain 0.6.0.dev109 documentation</title>
88
<link rel="stylesheet" type="text/css" href="_static/pygments.css?v=b86133f3" />
99
<link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
1010
<link rel="stylesheet" type="text/css" href="_static/platformpicker.css" />
@@ -17,10 +17,11 @@
1717

1818
<script src="_static/jquery.js?v=5d32c60e"></script>
1919
<script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
20-
<script src="_static/documentation_options.js?v=3c567cdd"></script>
20+
<script src="_static/documentation_options.js?v=982ef8c4"></script>
2121
<script src="_static/doctools.js?v=9a2dae69"></script>
2222
<script src="_static/sphinx_highlight.js?v=dc90522c"></script>
2323
<script src="_static/platformpicker.js"></script>
24+
<script src="_static/version-switch.js?v=6c8574fb"></script>
2425
<script src="_static/js/theme.js"></script>
2526
<link rel="index" title="Index" href="genindex.html" />
2627
<link rel="search" title="Search" href="search.html" />
@@ -41,7 +42,7 @@
4142
<img src="_static/logo.png" class="logo" alt="Logo"/>
4243
</a>
4344
<div class="version">
44-
0.6.0.dev108
45+
0.6.0.dev109
4546
</div>
4647
<div role="search">
4748
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">

docs/amaranth/latest/index.html

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />
55

66
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
7-
<title>Language &amp; toolchain &mdash; Amaranth language &amp; toolchain 0.6.0.dev108 documentation</title>
7+
<title>Language &amp; toolchain &mdash; Amaranth language &amp; toolchain 0.6.0.dev109 documentation</title>
88
<link rel="stylesheet" type="text/css" href="_static/pygments.css?v=b86133f3" />
99
<link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
1010
<link rel="stylesheet" type="text/css" href="_static/platformpicker.css" />
@@ -17,10 +17,11 @@
1717

1818
<script src="_static/jquery.js?v=5d32c60e"></script>
1919
<script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
20-
<script src="_static/documentation_options.js?v=3c567cdd"></script>
20+
<script src="_static/documentation_options.js?v=982ef8c4"></script>
2121
<script src="_static/doctools.js?v=9a2dae69"></script>
2222
<script src="_static/sphinx_highlight.js?v=dc90522c"></script>
2323
<script src="_static/platformpicker.js"></script>
24+
<script src="_static/version-switch.js?v=6c8574fb"></script>
2425
<script src="_static/js/theme.js"></script>
2526
<link rel="index" title="Index" href="genindex.html" />
2627
<link rel="search" title="Search" href="search.html" />
@@ -41,7 +42,7 @@
4142
<img src="_static/logo.png" class="logo" alt="Logo"/>
4243
</a>
4344
<div class="version">
44-
0.6.0.dev108
45+
0.6.0.dev109
4546
</div>
4647
<div role="search">
4748
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">

docs/amaranth/latest/install.html

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />
55

66
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
7-
<title>Installation &mdash; Amaranth language &amp; toolchain 0.6.0.dev108 documentation</title>
7+
<title>Installation &mdash; Amaranth language &amp; toolchain 0.6.0.dev109 documentation</title>
88
<link rel="stylesheet" type="text/css" href="_static/pygments.css?v=b86133f3" />
99
<link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
1010
<link rel="stylesheet" type="text/css" href="_static/platformpicker.css" />
@@ -17,10 +17,11 @@
1717

1818
<script src="_static/jquery.js?v=5d32c60e"></script>
1919
<script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
20-
<script src="_static/documentation_options.js?v=3c567cdd"></script>
20+
<script src="_static/documentation_options.js?v=982ef8c4"></script>
2121
<script src="_static/doctools.js?v=9a2dae69"></script>
2222
<script src="_static/sphinx_highlight.js?v=dc90522c"></script>
2323
<script src="_static/platformpicker.js"></script>
24+
<script src="_static/version-switch.js?v=6c8574fb"></script>
2425
<script src="_static/js/theme.js"></script>
2526
<link rel="index" title="Index" href="genindex.html" />
2627
<link rel="search" title="Search" href="search.html" />
@@ -41,7 +42,7 @@
4142
<img src="_static/logo.png" class="logo" alt="Logo"/>
4243
</a>
4344
<div class="version">
44-
0.6.0.dev108
45+
0.6.0.dev109
4546
</div>
4647
<div role="search">
4748
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">

0 commit comments

Comments
 (0)