build based on fda016f

This commit is contained in:
Documenter.jl 2024-05-07 02:53:43 +00:00
parent 1a34b32304
commit 1d29bc3418
19 changed files with 1632 additions and 3 deletions

View file

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

1
stable Symbolic link
View file

@ -0,0 +1 @@
v0.1.0

1
v0.1 Symbolic link
View file

@ -0,0 +1 @@
v0.1.0

View file

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

1050
v0.1.0/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

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
v0.1.0/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
v0.1.0/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
v0.1.0/index.html Normal file

File diff suppressed because one or more lines are too long

BIN
v0.1.0/objects.inv Normal file

Binary file not shown.

File diff suppressed because one or more lines are too long

3
v0.1.0/search_index.js Normal file

File diff suppressed because one or more lines are too long

1
v0.1.0/siteinfo.js Normal file
View file

@ -0,0 +1 @@
var DOCUMENTER_CURRENT_VERSION = "v0.1.0";

View file

@ -1,5 +1,7 @@
var DOC_VERSIONS = [ var DOC_VERSIONS = [
"stable",
"v0.1",
"dev", "dev",
]; ];
var DOCUMENTER_NEWEST = "dev"; var DOCUMENTER_NEWEST = "v0.1.0";
var DOCUMENTER_STABLE = "dev"; var DOCUMENTER_STABLE = "stable";