Skip to content

Commit 9ca6be0

Browse files
GH Actions RunnerGH Actions Runner
GH Actions Runner
authored and
GH Actions Runner
committed
publish: Merge pull request #50 from JohnTitor/tweak-gha
generated from commit a828e32
1 parent 76118a9 commit 9ca6be0

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

49 files changed

+691
-712
lines changed

‎404.html

Lines changed: 13 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@
99

1010
<!-- Custom HTML head -->
1111

12-
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
1312
<meta name="description" content="Guide for standard library developers">
1413
<meta name="viewport" content="width=device-width, initial-scale=1">
1514
<meta name="theme-color" content="#ffffff" />
@@ -35,13 +34,13 @@
3534
</head>
3635
<body>
3736
<!-- Provide site root to javascript -->
38-
<script type="text/javascript">
37+
<script>
3938
var path_to_root = "";
4039
var default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? "navy" : "light";
4140
</script>
4241

4342
<!-- Work around some values being stored in localStorage wrapped in quotes -->
44-
<script type="text/javascript">
43+
<script>
4544
try {
4645
var theme = localStorage.getItem('mdbook-theme');
4746
var sidebar = localStorage.getItem('mdbook-sidebar');
@@ -57,7 +56,7 @@
5756
</script>
5857

5958
<!-- Set the theme before any content is loaded, prevents flash -->
60-
<script type="text/javascript">
59+
<script>
6160
var theme;
6261
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
6362
if (theme === null || theme === undefined) { theme = default_theme; }
@@ -69,7 +68,7 @@
6968
</script>
7069

7170
<!-- Hide / unhide sidebar before it is displayed -->
72-
<script type="text/javascript">
71+
<script>
7372
var html = document.querySelector('html');
7473
var sidebar = 'hidden';
7574
if (document.body.clientWidth >= 1080) {
@@ -100,7 +99,7 @@
10099
<i class="fa fa-paint-brush"></i>
101100
</button>
102101
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
103-
<li role="none"><button role="menuitem" class="theme" id="light">Light (default)</button></li>
102+
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
104103
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
105104
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
106105
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
@@ -136,7 +135,7 @@ <h1 class="menu-title">Standard library developers Guide</h1>
136135
</div>
137136

138137
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
139-
<script type="text/javascript">
138+
<script>
140139
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
141140
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
142141
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
@@ -169,18 +168,18 @@ <h1 id="document-not-found-404"><a class="header" href="#document-not-found-404"
169168

170169

171170

172-
<script type="text/javascript">
171+
<script>
173172
window.playground_copyable = true;
174173
</script>
175174

176175

177-
<script src="elasticlunr.min.js" type="text/javascript" charset="utf-8"></script>
178-
<script src="mark.min.js" type="text/javascript" charset="utf-8"></script>
179-
<script src="searcher.js" type="text/javascript" charset="utf-8"></script>
176+
<script src="elasticlunr.min.js"></script>
177+
<script src="mark.min.js"></script>
178+
<script src="searcher.js"></script>
180179

181-
<script src="clipboard.min.js" type="text/javascript" charset="utf-8"></script>
182-
<script src="highlight.js" type="text/javascript" charset="utf-8"></script>
183-
<script src="book.js" type="text/javascript" charset="utf-8"></script>
180+
<script src="clipboard.min.js"></script>
181+
<script src="highlight.js"></script>
182+
<script src="book.js"></script>
184183

185184
<!-- Custom JS scripts -->
186185

‎about-this-guide.html

Lines changed: 13 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@
88

99
<!-- Custom HTML head -->
1010

11-
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
1211
<meta name="description" content="Guide for standard library developers">
1312
<meta name="viewport" content="width=device-width, initial-scale=1">
1413
<meta name="theme-color" content="#ffffff" />
@@ -34,13 +33,13 @@
3433
</head>
3534
<body>
3635
<!-- Provide site root to javascript -->
37-
<script type="text/javascript">
36+
<script>
3837
var path_to_root = "";
3938
var default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? "navy" : "light";
4039
</script>
4140

4241
<!-- Work around some values being stored in localStorage wrapped in quotes -->
43-
<script type="text/javascript">
42+
<script>
4443
try {
4544
var theme = localStorage.getItem('mdbook-theme');
4645
var sidebar = localStorage.getItem('mdbook-sidebar');
@@ -56,7 +55,7 @@
5655
</script>
5756

5857
<!-- Set the theme before any content is loaded, prevents flash -->
59-
<script type="text/javascript">
58+
<script>
6059
var theme;
6160
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
6261
if (theme === null || theme === undefined) { theme = default_theme; }
@@ -68,7 +67,7 @@
6867
</script>
6968

7069
<!-- Hide / unhide sidebar before it is displayed -->
71-
<script type="text/javascript">
70+
<script>
7271
var html = document.querySelector('html');
7372
var sidebar = 'hidden';
7473
if (document.body.clientWidth >= 1080) {
@@ -99,7 +98,7 @@
9998
<i class="fa fa-paint-brush"></i>
10099
</button>
101100
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
102-
<li role="none"><button role="menuitem" class="theme" id="light">Light (default)</button></li>
101+
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
103102
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
104103
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
105104
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
@@ -138,7 +137,7 @@ <h1 class="menu-title">Standard library developers Guide</h1>
138137
</div>
139138

140139
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
141-
<script type="text/javascript">
140+
<script>
142141
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
143142
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
144143
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
@@ -186,18 +185,18 @@ <h2 id="other-places-to-find-information"><a class="header" href="#other-places-
186185

187186

188187

189-
<script type="text/javascript">
188+
<script>
190189
window.playground_copyable = true;
191190
</script>
192191

193192

194-
<script src="elasticlunr.min.js" type="text/javascript" charset="utf-8"></script>
195-
<script src="mark.min.js" type="text/javascript" charset="utf-8"></script>
196-
<script src="searcher.js" type="text/javascript" charset="utf-8"></script>
193+
<script src="elasticlunr.min.js"></script>
194+
<script src="mark.min.js"></script>
195+
<script src="searcher.js"></script>
197196

198-
<script src="clipboard.min.js" type="text/javascript" charset="utf-8"></script>
199-
<script src="highlight.js" type="text/javascript" charset="utf-8"></script>
200-
<script src="book.js" type="text/javascript" charset="utf-8"></script>
197+
<script src="clipboard.min.js"></script>
198+
<script src="highlight.js"></script>
199+
<script src="book.js"></script>
201200

202201
<!-- Custom JS scripts -->
203202

‎ayu-highlight.css

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ Original by Dempfi (https://github.com/dempfi/ayu)
88
overflow-x: auto;
99
background: #191f26;
1010
color: #e6e1cf;
11-
padding: 0.5em;
1211
}
1312

1413
.hljs-comment,

‎book.js

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,14 +4,16 @@
44
window.onunload = function () { };
55

66
// Global variable, shared between modules
7-
function playground_text(playground) {
7+
function playground_text(playground, hidden = true) {
88
let code_block = playground.querySelector("code");
99

1010
if (window.ace && code_block.classList.contains("editable")) {
1111
let editor = window.ace.edit(code_block);
1212
return editor.getValue();
13-
} else {
13+
} else if (hidden) {
1414
return code_block.textContent;
15+
} else {
16+
return code_block.innerText;
1517
}
1618
}
1719

@@ -166,7 +168,6 @@ function playground_text(playground) {
166168
.filter(function (node) {return node.classList.contains("editable"); })
167169
.forEach(function (block) { block.classList.remove('language-rust'); });
168170

169-
Array
170171
code_nodes
171172
.filter(function (node) {return !node.classList.contains("editable"); })
172173
.forEach(function (block) { hljs.highlightBlock(block); });
@@ -300,6 +301,13 @@ function playground_text(playground) {
300301
themePopup.querySelector("button#" + get_theme()).focus();
301302
}
302303

304+
function updateThemeSelected() {
305+
themePopup.querySelectorAll('.theme-selected').forEach(function (el) {
306+
el.classList.remove('theme-selected');
307+
});
308+
themePopup.querySelector("button#" + get_theme()).classList.add('theme-selected');
309+
}
310+
303311
function hideThemes() {
304312
themePopup.style.display = 'none';
305313
themeToggleButton.setAttribute('aria-expanded', false);
@@ -355,6 +363,7 @@ function playground_text(playground) {
355363

356364
html.classList.remove(previousTheme);
357365
html.classList.add(theme);
366+
updateThemeSelected();
358367
}
359368

360369
// Set theme
@@ -592,7 +601,7 @@ function playground_text(playground) {
592601
text: function (trigger) {
593602
hideTooltip(trigger);
594603
let playground = trigger.closest("pre");
595-
return playground_text(playground);
604+
return playground_text(playground, false);
596605
}
597606
});
598607

‎code-considerations/breaking-changes/behavior.html

Lines changed: 13 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@
88

99
<!-- Custom HTML head -->
1010

11-
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
1211
<meta name="description" content="Guide for standard library developers">
1312
<meta name="viewport" content="width=device-width, initial-scale=1">
1413
<meta name="theme-color" content="#ffffff" />
@@ -34,13 +33,13 @@
3433
</head>
3534
<body>
3635
<!-- Provide site root to javascript -->
37-
<script type="text/javascript">
36+
<script>
3837
var path_to_root = "../../";
3938
var default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? "navy" : "light";
4039
</script>
4140

4241
<!-- Work around some values being stored in localStorage wrapped in quotes -->
43-
<script type="text/javascript">
42+
<script>
4443
try {
4544
var theme = localStorage.getItem('mdbook-theme');
4645
var sidebar = localStorage.getItem('mdbook-sidebar');
@@ -56,7 +55,7 @@
5655
</script>
5756

5857
<!-- Set the theme before any content is loaded, prevents flash -->
59-
<script type="text/javascript">
58+
<script>
6059
var theme;
6160
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
6261
if (theme === null || theme === undefined) { theme = default_theme; }
@@ -68,7 +67,7 @@
6867
</script>
6968

7069
<!-- Hide / unhide sidebar before it is displayed -->
71-
<script type="text/javascript">
70+
<script>
7271
var html = document.querySelector('html');
7372
var sidebar = 'hidden';
7473
if (document.body.clientWidth >= 1080) {
@@ -99,7 +98,7 @@
9998
<i class="fa fa-paint-brush"></i>
10099
</button>
101100
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
102-
<li role="none"><button role="menuitem" class="theme" id="light">Light (default)</button></li>
101+
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
103102
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
104103
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
105104
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
@@ -138,7 +137,7 @@ <h1 class="menu-title">Standard library developers Guide</h1>
138137
</div>
139138

140139
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
141-
<script type="text/javascript">
140+
<script>
142141
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
143142
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
144143
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
@@ -186,18 +185,18 @@ <h2 id="for-reviewers"><a class="header" href="#for-reviewers">For reviewers</a>
186185

187186

188187

189-
<script type="text/javascript">
188+
<script>
190189
window.playground_copyable = true;
191190
</script>
192191

193192

194-
<script src="../../elasticlunr.min.js" type="text/javascript" charset="utf-8"></script>
195-
<script src="../../mark.min.js" type="text/javascript" charset="utf-8"></script>
196-
<script src="../../searcher.js" type="text/javascript" charset="utf-8"></script>
193+
<script src="../../elasticlunr.min.js"></script>
194+
<script src="../../mark.min.js"></script>
195+
<script src="../../searcher.js"></script>
197196

198-
<script src="../../clipboard.min.js" type="text/javascript" charset="utf-8"></script>
199-
<script src="../../highlight.js" type="text/javascript" charset="utf-8"></script>
200-
<script src="../../book.js" type="text/javascript" charset="utf-8"></script>
197+
<script src="../../clipboard.min.js"></script>
198+
<script src="../../highlight.js"></script>
199+
<script src="../../book.js"></script>
201200

202201
<!-- Custom JS scripts -->
203202

0 commit comments

Comments
 (0)