build based on 90a92d7

dev/.documenter-siteinfo.json

@@ -0,0 +1 @@
+{"documenter":{"julia_version":"1.10.5","generation_timestamp":"2024-09-28T22:13:29","documenter_version":"1.7.0"}}

dev/assets/search.js

@@ -1,267 +0,0 @@
-// Generated by Documenter.jl
-requirejs.config({
-  paths: {
-    'lunr': 'https://cdnjs.cloudflare.com/ajax/libs/lunr.js/2.3.9/lunr.min',
-    'lodash': 'https://cdnjs.cloudflare.com/ajax/libs/lodash.js/4.17.21/lodash.min',
-    'jquery': 'https://cdnjs.cloudflare.com/ajax/libs/jquery/3.6.4/jquery.min',
-  }
-});
-////////////////////////////////////////////////////////////////////////////////
-require(['jquery', 'lunr', 'lodash'], function($, lunr, _) {
-
-$(document).ready(function() {
-  // parseUri 1.2.2
-  // (c) Steven Levithan <stevenlevithan.com>
-  // MIT License
-  function parseUri (str) {
-    var  o   = parseUri.options,
-      m   = o.parser[o.strictMode ? "strict" : "loose"].exec(str),
-      uri = {},
-      i   = 14;
-
-    while (i--) uri[o.key[i]] = m[i] || "";
-
-    uri[o.q.name] = {};
-    uri[o.key[12]].replace(o.q.parser, function ($0, $1, $2) {
-      if ($1) uri[o.q.name][$1] = $2;
-    });
-
-    return uri;
-  };
-  parseUri.options = {
-    strictMode: false,
-    key: ["source","protocol","authority","userInfo","user","password","host","port","relative","path","directory","file","query","anchor"],
-    q:   {
-      name:   "queryKey",
-      parser: /(?:^|&)([^&=]*)=?([^&]*)/g
-    },
-    parser: {
-      strict: /^(?:([^:\/?#]+):)?(?:\/\/((?:(([^:@]*)(?::([^:@]*))?)?@)?([^:\/?#]*)(?::(\d*))?))?((((?:[^?#\/]*\/)*)([^?#]*))(?:\?([^#]*))?(?:#(.*))?)/,
-      loose:  /^(?:(?![^:@]+:[^:@\/]*@)([^:\/?#.]+):)?(?:\/\/)?((?:(([^:@]*)(?::([^:@]*))?)?@)?([^:\/?#]*)(?::(\d*))?)(((\/(?:[^?#](?![^?#\/]*\.[^?#\/.]+(?:[?#]|$)))*\/?)?([^?#\/]*))(?:\?([^#]*))?(?:#(.*))?)/
-    }
-  };
-
-  $("#search-form").submit(function(e) {
-    e.preventDefault()
-  })
-
-  // list below is the lunr 2.1.3 list minus the intersect with names(Base)
-  // (all, any, get, in, is, only, which) and (do, else, for, let, where, while, with)
-  // ideally we'd just filter the original list but it's not available as a variable
-  lunr.stopWordFilter = lunr.generateStopWordFilter([
-    'a',
-    'able',
-    'about',
-    'across',
-    'after',
-    'almost',
-    'also',
-    'am',
-    'among',
-    'an',
-    'and',
-    'are',
-    'as',
-    'at',
-    'be',
-    'because',
-    'been',
-    'but',
-    'by',
-    'can',
-    'cannot',
-    'could',
-    'dear',
-    'did',
-    'does',
-    'either',
-    'ever',
-    'every',
-    'from',
-    'got',
-    'had',
-    'has',
-    'have',
-    'he',
-    'her',
-    'hers',
-    'him',
-    'his',
-    'how',
-    'however',
-    'i',
-    'if',
-    'into',
-    'it',
-    'its',
-    'just',
-    'least',
-    'like',
-    'likely',
-    'may',
-    'me',
-    'might',
-    'most',
-    'must',
-    'my',
-    'neither',
-    'no',
-    'nor',
-    'not',
-    'of',
-    'off',
-    'often',
-    'on',
-    'or',
-    'other',
-    'our',
-    'own',
-    'rather',
-    'said',
-    'say',
-    'says',
-    'she',
-    'should',
-    'since',
-    'so',
-    'some',
-    'than',
-    'that',
-    'the',
-    'their',
-    'them',
-    'then',
-    'there',
-    'these',
-    'they',
-    'this',
-    'tis',
-    'to',
-    'too',
-    'twas',
-    'us',
-    'wants',
-    'was',
-    'we',
-    'were',
-    'what',
-    'when',
-    'who',
-    'whom',
-    'why',
-    'will',
-    'would',
-    'yet',
-    'you',
-    'your'
-  ])
-
-  // add . as a separator, because otherwise "title": "Documenter.Anchors.add!"
-  // would not find anything if searching for "add!", only for the entire qualification
-  lunr.tokenizer.separator = /[\s\-\.]+/
-
-  // custom trimmer that doesn't strip @ and !, which are used in julia macro and function names
-  lunr.trimmer = function (token) {
-    return token.update(function (s) {
-      return s.replace(/^[^a-zA-Z0-9@!]+/, '').replace(/[^a-zA-Z0-9@!]+$/, '')
-    })
-  }
-
-  lunr.Pipeline.registerFunction(lunr.stopWordFilter, 'juliaStopWordFilter')
-  lunr.Pipeline.registerFunction(lunr.trimmer, 'juliaTrimmer')
-
-  var index = lunr(function () {
-    this.ref('location')
-    this.field('title',{boost: 100})
-    this.field('text')
-    documenterSearchIndex['docs'].forEach(function(e) {
-        this.add(e)
-    }, this)
-  })
-  var store = {}
-
-  documenterSearchIndex['docs'].forEach(function(e) {
-      store[e.location] = {title: e.title, category: e.category, page: e.page}
-  })
-
-  $(function(){
-    searchresults = $('#documenter-search-results');
-    searchinfo = $('#documenter-search-info');
-    searchbox = $('#documenter-search-query');
-    searchform = $('.docs-search');
-    sidebar = $('.docs-sidebar');
-    function update_search(querystring) {
-      tokens = lunr.tokenizer(querystring)
-      results = index.query(function (q) {
-        tokens.forEach(function (t) {
-          q.term(t.toString(), {
-            fields: ["title"],
-            boost: 100,
-            usePipeline: true,
-            editDistance: 0,
-            wildcard: lunr.Query.wildcard.NONE
-          })
-          q.term(t.toString(), {
-            fields: ["title"],
-            boost: 10,
-            usePipeline: true,
-            editDistance: 2,
-            wildcard: lunr.Query.wildcard.NONE
-          })
-          q.term(t.toString(), {
-            fields: ["text"],
-            boost: 1,
-            usePipeline: true,
-            editDistance: 0,
-            wildcard: lunr.Query.wildcard.NONE
-          })
-        })
-      })
-      searchinfo.text("Number of results: " + results.length)
-      searchresults.empty()
-      results.forEach(function(result) {
-        data = store[result.ref]
-        link = $('<a class="docs-label">'+data.title+'</a>')
-        link.attr('href', documenterBaseURL+'/'+result.ref)
-        if (data.category != "page"){
-          cat = $('<span class="docs-category">('+data.category+', '+data.page+')</span>')
-        } else {
-          cat = $('<span class="docs-category">('+data.category+')</span>')
-        }
-        li = $('<li>').append(link).append(" ").append(cat)
-        searchresults.append(li)
-      })
-    }
-
-    function update_search_box() {
-      querystring = searchbox.val()
-      update_search(querystring)
-    }
-
-    searchbox.keyup(_.debounce(update_search_box, 250))
-    searchbox.change(update_search_box)
-
-    // Disable enter-key form submission for the searchbox on the search page
-    // and just re-run search rather than refresh the whole page.
-    searchform.keypress(
-      function(event){
-        if (event.which == '13') {
-          if (sidebar.hasClass('visible')) {
-            sidebar.removeClass('visible');
-          }
-          update_search_box();
-          event.preventDefault();
-        }
-      }
-    );
-
-    search_query_uri = parseUri(window.location).queryKey["q"]
-    if(search_query_uri !== undefined) {
-      search_query = decodeURIComponent(search_query_uri.replace(/\+/g, '%20'))
-      searchbox.val(search_query)
-    }
-    update_search_box();
-  })
-})
-
-})

dev/assets/themeswap.js

@@ -4,17 +4,14 @@ function set_theme_from_local_storage() {
   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();

dev/assets/warner.js

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