build based on 26303f3

This commit is contained in:
Documenter.jl 2024-05-07 02:47:03 +00:00
parent 29b9131c03
commit 75cf80bf38
17 changed files with 1632 additions and 0 deletions

View file

@ -0,0 +1 @@
{"documenter":{"julia_version":"1.10.3","generation_timestamp":"2024-05-07T02:47:00","documenter_version":"1.4.1"}}

1050
dev/assets/documenter.js Normal file

File diff suppressed because it is too large Load diff

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

84
dev/assets/themeswap.js Normal file
View file

@ -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();

52
dev/assets/warner.js Normal file
View file

@ -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

167
dev/distance/index.html Normal file

File diff suppressed because one or more lines are too long

Binary file not shown.

After

Width:  |  Height:  |  Size: 32 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 72 KiB

155
dev/index.html Normal file

File diff suppressed because one or more lines are too long

BIN
dev/objects.inv Normal file

Binary file not shown.

52
dev/pauliops/index.html Normal file

File diff suppressed because one or more lines are too long

3
dev/search_index.js Normal file

File diff suppressed because one or more lines are too long

1
dev/siteinfo.js Normal file
View file

@ -0,0 +1 @@
var DOCUMENTER_CURRENT_VERSION = "dev";

2
index.html Normal file
View file

@ -0,0 +1,2 @@
<!--This file is automatically generated by Documenter.jl-->
<meta http-equiv="refresh" content="0; url=./dev/"/>

5
versions.js Normal file
View file

@ -0,0 +1,5 @@
var DOC_VERSIONS = [
"dev",
];
var DOCUMENTER_NEWEST = "dev";
var DOCUMENTER_STABLE = "dev";