Documenter.jl
1 year ago
13 changed files with 1285 additions and 2 deletions
@ -0,0 +1 @@
@@ -0,0 +1 @@
|
||||
{"documenter":{"julia_version":"1.10.4","generation_timestamp":"2024-07-12T13:15:32","documenter_version":"1.4.0"}} |
||||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
@ -0,0 +1,84 @@
@@ -0,0 +1,84 @@
|
||||
// Small function to quickly swap out themes. Gets put into the <head> tag..
|
||||
function set_theme_from_local_storage() { |
||||
// Initialize the theme to null, which means default
|
||||
var theme = null; |
||||
// If the browser supports the localstorage and is not disabled then try to get the
|
||||
// documenter theme
|
||||
if (window.localStorage != null) { |
||||
// Get the user-picked theme from localStorage. May be `null`, which means the default
|
||||
// theme.
|
||||
theme = window.localStorage.getItem("documenter-theme"); |
||||
} |
||||
// Check if the users preference is for dark color scheme
|
||||
var darkPreference = |
||||
window.matchMedia("(prefers-color-scheme: dark)").matches === true; |
||||
// Initialize a few variables for the loop:
|
||||
//
|
||||
// - active: will contain the index of the theme that should be active. Note that there
|
||||
// is no guarantee that localStorage contains sane values. If `active` stays `null`
|
||||
// we either could not find the theme or it is the default (primary) theme anyway.
|
||||
// Either way, we then need to stick to the primary theme.
|
||||
//
|
||||
// - disabled: style sheets that should be disabled (i.e. all the theme style sheets
|
||||
// that are not the currently active theme)
|
||||
var active = null; |
||||
var disabled = []; |
||||
var primaryLightTheme = null; |
||||
var primaryDarkTheme = null; |
||||
for (var i = 0; i < document.styleSheets.length; i++) { |
||||
var ss = document.styleSheets[i]; |
||||
// The <link> tag of each style sheet is expected to have a data-theme-name attribute
|
||||
// which must contain the name of the theme. The names in localStorage much match this.
|
||||
var themename = ss.ownerNode.getAttribute("data-theme-name"); |
||||
// attribute not set => non-theme stylesheet => ignore
|
||||
if (themename === null) continue; |
||||
// To distinguish the default (primary) theme, it needs to have the data-theme-primary
|
||||
// attribute set.
|
||||
if (ss.ownerNode.getAttribute("data-theme-primary") !== null) { |
||||
primaryLightTheme = themename; |
||||
} |
||||
// Check if the theme is primary dark theme so that we could store its name in darkTheme
|
||||
if (ss.ownerNode.getAttribute("data-theme-primary-dark") !== null) { |
||||
primaryDarkTheme = themename; |
||||
} |
||||
// If we find a matching theme (and it's not the default), we'll set active to non-null
|
||||
if (themename === theme) active = i; |
||||
// Store the style sheets of inactive themes so that we could disable them
|
||||
if (themename !== theme) disabled.push(ss); |
||||
} |
||||
var activeTheme = null; |
||||
if (active !== null) { |
||||
// If we did find an active theme, we'll (1) add the theme--$(theme) class to <html>
|
||||
document.getElementsByTagName("html")[0].className = "theme--" + theme; |
||||
activeTheme = theme; |
||||
} else { |
||||
// If we did _not_ find an active theme, then we need to fall back to the primary theme
|
||||
// which can either be dark or light, depending on the user's OS preference.
|
||||
var activeTheme = darkPreference ? primaryDarkTheme : primaryLightTheme; |
||||
// In case it somehow happens that the relevant primary theme was not found in the
|
||||
// preceding loop, we abort without doing anything.
|
||||
if (activeTheme === null) { |
||||
console.error("Unable to determine primary theme."); |
||||
return; |
||||
} |
||||
// When switching to the primary light theme, then we must not have a class name
|
||||
// for the <html> tag. That's only for non-primary or the primary dark theme.
|
||||
if (darkPreference) { |
||||
document.getElementsByTagName("html")[0].className = |
||||
"theme--" + activeTheme; |
||||
} else { |
||||
document.getElementsByTagName("html")[0].className = ""; |
||||
} |
||||
} |
||||
for (var i = 0; i < document.styleSheets.length; i++) { |
||||
var ss = document.styleSheets[i]; |
||||
// The <link> tag of each style sheet is expected to have a data-theme-name attribute
|
||||
// which must contain the name of the theme. The names in localStorage much match this.
|
||||
var themename = ss.ownerNode.getAttribute("data-theme-name"); |
||||
// attribute not set => non-theme stylesheet => ignore
|
||||
if (themename === null) continue; |
||||
// we'll disable all the stylesheets, except for the active one
|
||||
ss.disabled = !(themename == activeTheme); |
||||
} |
||||
} |
||||
set_theme_from_local_storage(); |
||||
@ -0,0 +1,52 @@
@@ -0,0 +1,52 @@
|
||||
function maybeAddWarning() { |
||||
// DOCUMENTER_NEWEST is defined in versions.js, DOCUMENTER_CURRENT_VERSION and DOCUMENTER_STABLE
|
||||
// in siteinfo.js.
|
||||
// If either of these are undefined something went horribly wrong, so we abort.
|
||||
if ( |
||||
window.DOCUMENTER_NEWEST === undefined || |
||||
window.DOCUMENTER_CURRENT_VERSION === undefined || |
||||
window.DOCUMENTER_STABLE === undefined |
||||
) { |
||||
return; |
||||
} |
||||
|
||||
// Current version is not a version number, so we can't tell if it's the newest version. Abort.
|
||||
if (!/v(\d+\.)*\d+/.test(window.DOCUMENTER_CURRENT_VERSION)) { |
||||
return; |
||||
} |
||||
|
||||
// Current version is newest version, so no need to add a warning.
|
||||
if (window.DOCUMENTER_NEWEST === window.DOCUMENTER_CURRENT_VERSION) { |
||||
return; |
||||
} |
||||
|
||||
// Add a noindex meta tag (unless one exists) so that search engines don't index this version of the docs.
|
||||
if (document.body.querySelector('meta[name="robots"]') === null) { |
||||
const meta = document.createElement("meta"); |
||||
meta.name = "robots"; |
||||
meta.content = "noindex"; |
||||
|
||||
document.getElementsByTagName("head")[0].appendChild(meta); |
||||
} |
||||
|
||||
const div = document.createElement("div"); |
||||
div.classList.add("outdated-warning-overlay"); |
||||
const closer = document.createElement("button"); |
||||
closer.classList.add("outdated-warning-closer", "delete"); |
||||
closer.addEventListener("click", function () { |
||||
document.body.removeChild(div); |
||||
}); |
||||
const href = window.documenterBaseURL + "/../" + window.DOCUMENTER_STABLE; |
||||
div.innerHTML = |
||||
'This documentation is not for the latest stable release, but for either the development version or an older release.<br><a href="' + |
||||
href + |
||||
'">Click here to go to the documentation for the latest stable release.</a>'; |
||||
div.appendChild(closer); |
||||
document.body.appendChild(div); |
||||
} |
||||
|
||||
if (document.readyState === "loading") { |
||||
document.addEventListener("DOMContentLoaded", maybeAddWarning); |
||||
} else { |
||||
maybeAddWarning(); |
||||
} |
||||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
@ -0,0 +1 @@
@@ -0,0 +1 @@
|
||||
var DOCUMENTER_CURRENT_VERSION = "v1.4.0"; |
||||
Loading…
Reference in new issue