Skip to content

Commit f217ea9

Browse files
authored
Add a Random Module button (UniMath#1918)
This PR adds a button to the top menu bar which takes the user to a random formalization module. Not terribly discoverable, but I think that should be fixed by a separate PR with a "how to use the website" guide which we're currently missing. <img width="541" height="121" alt="image" src="https://github.com/user-attachments/assets/4a6b8acf-d34d-4445-8027-48b85f350d28" />
1 parent d5dd07c commit f217ea9

1 file changed

Lines changed: 23 additions & 0 deletions

File tree

website/theme/index.hbs

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -166,6 +166,10 @@
166166
<i class="fa fa-search"></i>
167167
</button>
168168
{{/if}}
169+
<button id="random-page" class="icon-button" type="button" title="Random Agda module"
170+
aria-label="Go to a random Agda module" aria-expanded="false">
171+
<i class="fa fa-random"></i>
172+
</button>
169173
</div>
170174

171175
<h1 class="menu-title"><a href="HOME.html">{{ book_title }}</a></h1>
@@ -261,6 +265,25 @@
261265
{{/if}}
262266
</div>
263267

268+
<script>
269+
document.querySelector('#random-page').addEventListener('click', () => {
270+
// Skip meta pages, which all have names in capital letters
271+
const metaRegex = /[A-Z_]+(\.lagda)?\.html/;
272+
// Extract the module list from the sidebar, no point duplicating this data
273+
const allModules = Array.prototype.filter.call(
274+
document.querySelectorAll('#sidebar .chapter-item > a'),
275+
// Filter based on the unresolved attribute (i.e. the relative path)
276+
link => {
277+
const href = link.attributes.href;
278+
// Filter out chevron links and meta pages
279+
return href && !metaRegex.test(href.value);
280+
}
281+
);
282+
const chosen = allModules[Math.floor(Math.random() * (allModules.length + 1))];
283+
location.href = chosen.href;
284+
});
285+
</script>
286+
264287
{{#if live_reload_endpoint}}
265288
<!-- Livereload script (if served using the cli tool) -->
266289
<script>

0 commit comments

Comments
 (0)