mirror of https://github.com/fredrikekre/HYPRE.jl
Documenter.jl
1 year ago
18 changed files with 1339 additions and 0 deletions
@ -0,0 +1 @@
@@ -0,0 +1 @@
|
||||
{"documenter":{"julia_version":"1.10.5","generation_timestamp":"2024-09-28T21:52:04","documenter_version":"1.7.0"}} |
||||
File diff suppressed because one or more lines are too long
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
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
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
File diff suppressed because one or more lines are too long
Binary file not shown.
File diff suppressed because one or more lines are too long
@ -0,0 +1 @@
@@ -0,0 +1 @@
|
||||
var DOCUMENTER_CURRENT_VERSION = "previews/PR18"; |
||||
File diff suppressed because one or more lines are too long
Loading…
Reference in new issue