From 75d06a815329563752f450f5e0849c3bf231306f Mon Sep 17 00:00:00 2001
From: Calvin Lee <calvins.lee@utah.edu>
Date: Fri, 9 Jun 2023 13:26:17 -0700
Subject: [PATCH] hide color-changer if javascript is disabled

---
 DocGen4/Output/Navbar.lean | 2 +-
 static/color-scheme.js     | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index 37b0bb6..33f06f7 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -83,7 +83,7 @@ def navbar : BaseHtmlM Html := do
           -/
           <h3>Library</h3>
           {← moduleList}
-          <div id="settings">
+          <div id="settings" hidden="hidden">
             -- `input` is a void tag, but can be self-closed to make parsing easier.
             <h3>Color scheme</h3>
             <form id="color-theme-switcher">
diff --git a/static/color-scheme.js b/static/color-scheme.js
index 4a1b6da..cb3af0b 100644
--- a/static/color-scheme.js
+++ b/static/color-scheme.js
@@ -26,3 +26,6 @@ document.addEventListener("DOMContentLoaded", function() {
         setTheme(getTheme());
     })
 });
+
+// un-hide the colorscheme picker
+document.querySelector("#settings").removeAttribute('hidden');