From 5058f2b4fa28f7e1dcbf92337bd01bbacc65d72b Mon Sep 17 00:00:00 2001
From: James Jensen <git@jaj.sh>
Date: Fri, 3 Jul 2026 12:15:58 +0800
Subject: [PATCH 1/3] web: Add search field on narrow screens

Cf. #640. Closes #426.

This also hides all the search fields when js is disabled (since they
didn't do anything anyway), and replaces "back to index" on narrow
screens with a search box when js is enabled.
---
 support/web/js/prompt.tsx |  7 +++----
 support/web/template.html | 16 +++++++++++++---
 2 files changed, 16 insertions(+), 7 deletions(-)

diff --git a/support/web/js/prompt.tsx b/support/web/js/prompt.tsx
index 89eadbfe5..55637d2cd 100644
--- a/support/web/js/prompt.tsx
+++ b/support/web/js/prompt.tsx
@@ -351,10 +351,9 @@ document.addEventListener("DOMContentLoaded", () => {
     }
   });
 
-  const searchInputProxy = document.getElementById("search-box-proxy") as HTMLInputElement | null;
-  if (searchInputProxy) {
-    searchInputProxy.addEventListener("focus", () => startSearch());
-  }
+  document.getElementById("search-box-proxy")?.addEventListener("focus", () => startSearch())
+  document.getElementById("narrow-search-box-proxy")?.addEventListener("focus", () => startSearch())
+
 
   document.addEventListener("keydown", e => {
     if (e.key == "k" && isShortcut(e)) {
diff --git a/support/web/template.html b/support/web/template.html
index b526f3fc8..8dfd4f22e 100644
--- a/support/web/template.html
+++ b/support/web/template.html
@@ -50,6 +50,10 @@
       body span.reasoning-step .alternate {
         display: none;
       }
+
+      .search-form {
+        display: none !important;
+      }
     </style>
   </noscript>
 
@@ -120,11 +124,17 @@ <h3 class="Agda" style="margin-top: 0; margin-bottom: 0; white-space: pre;">
           <!-- Index return anchor (only if the page is not the index) -->
           $if(is-index)$
           $else$
-          <div id=return>
-            <a href="$base-url$/">back to index</a>
-          </div>
+          <noscript>
+            <div id=return>
+              <a href="$base-url$/">back to index</a>
+            </div>
+          </noscript>
           $endif$
 
+          <div class="search-form search-form-proxy mathpar" role="form">
+            <input id="narrow-search-box-proxy" type_="text" placeholder="Search..." autocomplete="off" tabindex="0" />
+          </div>
+
           <!-- Navbar equations control -->
           <span class="equations" style="display: flex; gap: 0.25em; flex-wrap: nowrap;">
             <input name=navbar-eqns type="checkbox" class="equations" id=navbar-eqns>

From 6d06713c3b4042da3840f74484f03f78b6a07c0d Mon Sep 17 00:00:00 2001
From: James Jensen <git@jaj.sh>
Date: Fri, 3 Jul 2026 16:45:07 +0800
Subject: [PATCH 2/3] fixup: Suggestions from @ncfavier

---
 support/web/css/default.scss | 11 +++++++++++
 support/web/js/prompt.tsx    |  2 +-
 support/web/template.html    | 24 +++++++++++-------------
 3 files changed, 23 insertions(+), 14 deletions(-)

diff --git a/support/web/css/default.scss b/support/web/css/default.scss
index 8753a8d2f..9da68e685 100644
--- a/support/web/css/default.scss
+++ b/support/web/css/default.scss
@@ -449,6 +449,17 @@ kbd {
   }
 }
 
+#article-nav-left {
+  display: flex;
+  gap: 16px;
+}
+
+#narrow-search-btn {
+  background-color: transparent;
+  border: none;
+  font-size: 24px;
+}
+
 
 @include mixins.widescreen {
   .narrow-only {
diff --git a/support/web/js/prompt.tsx b/support/web/js/prompt.tsx
index 55637d2cd..52d88c6ee 100644
--- a/support/web/js/prompt.tsx
+++ b/support/web/js/prompt.tsx
@@ -352,7 +352,7 @@ document.addEventListener("DOMContentLoaded", () => {
   });
 
   document.getElementById("search-box-proxy")?.addEventListener("focus", () => startSearch())
-  document.getElementById("narrow-search-box-proxy")?.addEventListener("focus", () => startSearch())
+  document.getElementById("narrow-search-btn")?.addEventListener("click", () => startSearch())
 
 
   document.addEventListener("keydown", e => {
diff --git a/support/web/template.html b/support/web/template.html
index 8dfd4f22e..df78fd9e7 100644
--- a/support/web/template.html
+++ b/support/web/template.html
@@ -51,7 +51,7 @@
         display: none;
       }
 
-      .search-form {
+      .js-only {
         display: none !important;
       }
     </style>
@@ -97,7 +97,7 @@ <h3 class="Agda" style="margin-top: 0; margin-bottom: 0; white-space: pre;">
           $endif$
 
           <!-- Navbar navigation (lol) -->
-          <div class="search-form search-form-proxy mathpar" role="form">
+          <div class="search-form search-form-proxy mathpar js-only" role="form">
             <input id="search-box-proxy" type_="text" placeholder="Search..." autocomplete="off" tabindex="0" />
           </div>
 
@@ -121,18 +121,16 @@ <h3 class="Agda" style="margin-top: 0; margin-bottom: 0; white-space: pre;">
       <article>
         <!-- Article navigation (narrow screens only) -->
         <div class="narrow-only" id="article-nav">
-          <!-- Index return anchor (only if the page is not the index) -->
-          $if(is-index)$
-          $else$
-          <noscript>
-            <div id=return>
-              <a href="$base-url$/">back to index</a>
+          <div id="article-nav-left">
+            <div class="mathpar">
+              <a id=logo href="$base-url$/">
+                <img alt="1Lab" src="$base-url$/static/cube-72x.png" style="display: block; margin-bottom: 1em; margin: auto;"
+                  width="32px" height="32px" />
+              </a>
+            </div>
+            <div class="mathpar js-only">
+              <button id="narrow-search-btn">🔍</button>
             </div>
-          </noscript>
-          $endif$
-
-          <div class="search-form search-form-proxy mathpar" role="form">
-            <input id="narrow-search-box-proxy" type_="text" placeholder="Search..." autocomplete="off" tabindex="0" />
           </div>
 
           <!-- Navbar equations control -->

From a5d137e2b4a28ac7fe7dab5bea3e7be3bcb651a8 Mon Sep 17 00:00:00 2001
From: James Jensen <git@jaj.sh>
Date: Sun, 5 Jul 2026 18:17:33 +0800
Subject: [PATCH 3/3] fixup: Trim forehead

---
 support/web/css/default.scss | 23 ++++++++++++-----------
 support/web/template.html    | 14 +++++---------
 2 files changed, 17 insertions(+), 20 deletions(-)

diff --git a/support/web/css/default.scss b/support/web/css/default.scss
index 9da68e685..46d362b29 100644
--- a/support/web/css/default.scss
+++ b/support/web/css/default.scss
@@ -337,6 +337,18 @@ article {
     flex-direction: row;
     justify-content: space-between;
     align-items: center;
+    margin-bottom: var(--parskip);
+
+    #article-nav-left {
+      display: flex;
+      gap: 16px;
+
+      #narrow-search-btn {
+        background-color: transparent;
+        border: none;
+        font-size: 24px;
+      }
+    }
   }
 
   > p {
@@ -449,17 +461,6 @@ kbd {
   }
 }
 
-#article-nav-left {
-  display: flex;
-  gap: 16px;
-}
-
-#narrow-search-btn {
-  background-color: transparent;
-  border: none;
-  font-size: 24px;
-}
-
 
 @include mixins.widescreen {
   .narrow-only {
diff --git a/support/web/template.html b/support/web/template.html
index df78fd9e7..c4ba46f36 100644
--- a/support/web/template.html
+++ b/support/web/template.html
@@ -122,15 +122,11 @@ <h3 class="Agda" style="margin-top: 0; margin-bottom: 0; white-space: pre;">
         <!-- Article navigation (narrow screens only) -->
         <div class="narrow-only" id="article-nav">
           <div id="article-nav-left">
-            <div class="mathpar">
-              <a id=logo href="$base-url$/">
-                <img alt="1Lab" src="$base-url$/static/cube-72x.png" style="display: block; margin-bottom: 1em; margin: auto;"
-                  width="32px" height="32px" />
-              </a>
-            </div>
-            <div class="mathpar js-only">
-              <button id="narrow-search-btn">🔍</button>
-            </div>
+            <a id=logo href="$base-url$/">
+              <img alt="1Lab" src="$base-url$/static/cube-72x.png" style="display: block; margin-bottom: 1em; margin: auto;"
+                width="32px" height="32px" />
+            </a>
+            <button id="narrow-search-btn" class="js-only">🔍</button>
           </div>
 
           <!-- Navbar equations control -->