@@ -325,7 +325,16 @@ if (document.readyState === "complete" ||
328+// Scroll to current document in nav list.
329+let docsNavScroll = function() {
330+ let docsDetails = document.querySelectorAll("nav ul details")
331+ for (let details in docsDetails) {
332+ if (docsDetails[details].open) docsDetails[details].scrollIntoView()
328if (window.location.href.includes("docs")) {
336if (window.location.href.includes("docs")) {
337+ // tooltip behaviour for standard library page
329 tippy('.tooltip', {
338 tippy('.tooltip', {
330 content(reference) {
339 content(reference) {
331 const title = reference.getAttribute('title')
340 const title = reference.getAttribute('title')
@@ -336,6 +345,8 @@ if (window.location.href.includes("docs")) {
336 animation: 'fade'
345 animation: 'fade'
348+ // on mobile, dropdown selections go to the option
339 let docsSelect = document.getElementById('docsSelect');
350 let docsSelect = document.getElementById('docsSelect');
340 let goTo = function() {
351 let goTo = function() {
341 let url = docsSelect.options[docsSelect.selectedIndex].value;
352 let url = docsSelect.options[docsSelect.selectedIndex].value;
@@ -345,6 +356,8 @@ if (window.location.href.includes("docs")) {
347 docsSelect.addEventListener('change', goTo);
358 docsSelect.addEventListener('change', goTo);
359+ // docs autoscroll to current page
350// same-page navigation on-scroll behaviour
363// same-page navigation on-scroll behaviour