Fix formatting issues in JS files

JuliaDocs · Nov 15, 2024 · f4556bd · f4556bd
1 parent 9e1b02f
commit f4556bd
Show file tree

Hide file tree

Showing 4 changed files with 33 additions and 33 deletions.
diff --git a/.prettierrc b/.prettierrc
@@ -1,11 +1,11 @@
 {
-  "tabWidth": 2,               
-  "semi": true,                
-  "singleQuote": true,          
-  "trailingComma": "es5",      
-  "bracketSpacing": true,      
-  "arrowParens": "always",      
-  "useTabs": false,             
-  "printWidth": 80,             
-  "endOfLine": "lf"             
+  "tabWidth": 2,
+  "semi": true,
+  "singleQuote": true,
+  "trailingComma": "es5",
+  "bracketSpacing": true,
+  "arrowParens": "always",
+  "useTabs": false,
+  "printWidth": 80,
+  "endOfLine": "lf"
 }
diff --git a/assets/html/themeswap.js b/assets/html/themeswap.js
@@ -7,11 +7,11 @@ function set_theme_from_local_storage() {
   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 users preference is for dark color scheme
   var darkPreference =
-    window.matchMedia("(prefers-color-scheme: dark)").matches === true;
+    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
@@ -29,16 +29,16 @@ function set_theme_from_local_storage() {
     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");
+    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) {
+    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) {
+    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
@@ -49,7 +49,7 @@ function set_theme_from_local_storage() {
   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;
+    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
@@ -58,23 +58,23 @@ function set_theme_from_local_storage() {
     // 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.");
+      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;
+      document.getElementsByTagName('html')[0].className =
+        'theme--' + activeTheme;
     } else {
-      document.getElementsByTagName("html")[0].className = "";
+      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");
+    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

diff --git a/assets/html/warner.js b/assets/html/warner.js
@@ -22,21 +22,21 @@ function maybeAddWarning() {
 
   // 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";
+    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 () {
+  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;
+  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 +
@@ -45,8 +45,8 @@ function maybeAddWarning() {
   document.body.appendChild(div);
 }
 
-if (document.readyState === "loading") {
-  document.addEventListener("DOMContentLoaded", maybeAddWarning);
+if (document.readyState === 'loading') {
+  document.addEventListener('DOMContentLoaded', maybeAddWarning);
 } else {
   maybeAddWarning();
 }
diff --git a/docs/versions.js b/docs/versions.js
@@ -1,3 +1,3 @@
 // This is here just to make the version selector show up when you build Documenter's
 // manual locally when developing / debugging.
-var DOC_VERSIONS = ["build"];
+var DOC_VERSIONS = ['build'];