Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
build based on 600b82c
Browse files Browse the repository at this point in the history
Documenter.jl committed Sep 30, 2024
1 parent c005757 commit 4db3077
Showing 20 changed files with 1,136 additions and 18,310 deletions.
1 change: 1 addition & 0 deletions dev/.documenter-siteinfo.json
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"documenter":{"julia_version":"1.10.5","generation_timestamp":"2024-09-30T15:32:12","documenter_version":"1.7.0"}}
472 changes: 6 additions & 466 deletions dev/api/index.html

Large diffs are not rendered by default.

927 changes: 830 additions & 97 deletions dev/assets/documenter.js

Large diffs are not rendered by default.

267 changes: 0 additions & 267 deletions dev/assets/search.js

This file was deleted.

1 change: 1 addition & 0 deletions dev/assets/themes/catppuccin-frappe.css

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions dev/assets/themes/catppuccin-latte.css

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions dev/assets/themes/catppuccin-macchiato.css

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions dev/assets/themes/catppuccin-mocha.css

Large diffs are not rendered by default.

7,699 changes: 2 additions & 7,697 deletions dev/assets/themes/documenter-dark.css

Large diffs are not rendered by default.

7,733 changes: 2 additions & 7,731 deletions dev/assets/themes/documenter-light.css

Large diffs are not rendered by default.

82 changes: 50 additions & 32 deletions dev/assets/themeswap.js
Original file line number Diff line number Diff line change
@@ -1,20 +1,17 @@
// Small function to quickly swap out themes. Gets put into the <head> tag..
function set_theme_from_local_storage() {
// Intialize the theme to null, which means default
// 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) {
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");
theme = window.localStorage.getItem("documenter-theme");
}
// Check if the browser supports user color preference
var darkPreference = false;
// Check if the users preference is for dark color scheme
if(window.matchMedia('(prefers-color-scheme: dark)').matches === true) {
darkPreference = true;
}
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
@@ -24,43 +21,64 @@ function set_theme_from_local_storage() {
//
// - 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 darkTheme = null;
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;
if (themename === null) continue;
// To distinguish the default (primary) theme, it needs to have the data-theme-primary
// attribute set.
var isprimary = (ss.ownerNode.getAttribute("data-theme-primary") !== null);
// Check if the theme is primary dark theme
var isDarkTheme = (ss.ownerNode.getAttribute("data-theme-primary-dark") !== null);
// If ss is for dark theme then set the value of darkTheme to the name of the theme
if(isDarkTheme) darkTheme = themename;
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;
if (themename === theme) active = i;
// Store the style sheets of inactive themes so that we could disable them
if(themename !== theme) disabled.push(ss);
if (themename !== theme) disabled.push(ss);
}
if(active !== null) {
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;
// and (2) disable all the other theme stylesheets
disabled.forEach(function(ss){
ss.disabled = true;
});
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 = "";
}
}
else if(darkTheme !== null && darkPreference === true) {
// If we did find an active theme, we'll (1) add the theme--$(theme) class to <html>
document.getElementsByTagName('html')[0].className = "theme--" + darkTheme;
// and (2) disable all the other theme stylesheets
disabled.forEach(function(ss){
if (ss.ownerNode.getAttribute("data-theme-name") !== darkTheme) {
ss.disabled = true;
}
});
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();
87 changes: 45 additions & 42 deletions dev/assets/warner.js
Original file line number Diff line number Diff line change
@@ -1,49 +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
};
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 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
};
// 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';
// 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);
};
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);
};
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);
if (document.readyState === "loading") {
document.addEventListener("DOMContentLoaded", maybeAddWarning);
} else {
maybeAddWarning();
};
maybeAddWarning();
}
46 changes: 46 additions & 0 deletions dev/getting-started/6de92eab.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
51 changes: 51 additions & 0 deletions dev/getting-started/f4cd06e4.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
70 changes: 70 additions & 0 deletions dev/getting-started/fa7b0e1c.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
1,081 changes: 27 additions & 1,054 deletions dev/getting-started/index.html

Large diffs are not rendered by default.

462 changes: 1 addition & 461 deletions dev/index.html

Large diffs are not rendered by default.

Binary file added dev/objects.inv
Binary file not shown.
462 changes: 0 additions & 462 deletions dev/search/index.html

This file was deleted.

2 changes: 1 addition & 1 deletion dev/search_index.js

Large diffs are not rendered by default.

0 comments on commit 4db3077

Please sign in to comment.