fix: scripts for search

Author: will-break-it

site/scripts/dev-with-formal-spec.sh

@@ -28,7 +28,7 @@ if [ -f "$SITE_DIR/static/agda_html/agda.css" ]; then
 fi
 
 # Copy all files except Agda.css
-cp -r result/html/* "$SITE_DIR/static/agda_html/"
+cp -r result/share/doc/agda/html/* "$SITE_DIR/static/agda_html/"
 
 # Restore our custom CSS
 if [ -f "$SITE_DIR/static/agda_html/agda.css.bak" ]; then

site/scripts/process-agda-html.js

@@ -151,50 +151,54 @@ if (searchInput && searchResults) {
 
   // Function to scroll to a specific line and highlight terms
   function scrollToLine(lineNumber, searchTerm) {
-    // Wait for the next frame to ensure content is rendered
-    requestAnimationFrame(() => {
-      const targetElement = document.querySelector('#L' + lineNumber);
-      if (targetElement) {
-        // Add a small delay to ensure content is fully rendered
-        setTimeout(() => {
-          targetElement.scrollIntoView({ behavior: 'smooth', block: 'center' });
-          targetElement.classList.add('highlight-line');
-          setTimeout(() => targetElement.classList.remove('highlight-line'), 2000);
-          
-          // Highlight all matching terms on the page
-          const content = document.querySelector('.agda-content');
-          if (content && searchTerm) {
-            const regex = new RegExp(searchTerm, 'gi');
-            const walker = document.createTreeWalker(content, NodeFilter.SHOW_TEXT, null, false);
-            const nodesToHighlight = [];
-            
-            while (walker.nextNode()) {
-              const node = walker.currentNode;
-              if (node.textContent.match(regex)) {
-                nodesToHighlight.push(node);
-              }
+    const targetElement = document.querySelector('.Agda .line:nth-child(' + (lineNumber - 1) + ')');
+    if (targetElement) {
+        // Remove any existing highlights
+        document.querySelectorAll('.line.highlight-line').forEach(line => {
+            line.classList.remove('highlight-line');
+        });
+
+        // Add highlight to target line
+        targetElement.classList.add('highlight-line');
+        
+        // Scroll to the line
+        targetElement.scrollIntoView({ behavior: 'smooth', block: 'center' });
+
+        // Highlight matching terms
+        if (searchTerm) {
+            const content = document.querySelector('.agda-content');
+            if (content) {
+                const regex = new RegExp(searchTerm, 'gi');
+                const walker = document.createTreeWalker(content, NodeFilter.SHOW_TEXT, null, false);
+                const nodesToHighlight = [];
+                
+                while (walker.nextNode()) {
+                    const node = walker.currentNode;
+                    if (node.textContent.match(regex)) {
+                        nodesToHighlight.push(node);
+                    }
+                }
+                
+                nodesToHighlight.forEach(node => {
+                    const span = document.createElement('span');
+                    span.className = 'search-term-highlight';
+                    span.innerHTML = node.textContent.replace(regex, match => '<mark>' + match + '</mark>');
+                    node.parentNode.replaceChild(span, node);
+                });
+                
+                // Remove highlights after 5 seconds
+                setTimeout(() => {
+                    const highlights = document.querySelectorAll('.search-term-highlight');
+                    highlights.forEach(highlight => {
+                        const text = highlight.textContent;
+                        const textNode = document.createTextNode(text);
+                        highlight.parentNode.replaceChild(textNode, highlight);
+                    });
+                    targetElement.classList.remove('highlight-line');
+                }, 5000);
             }
-            
-            nodesToHighlight.forEach(node => {
-              const span = document.createElement('span');
-              span.className = 'search-term-highlight';
-              span.innerHTML = node.textContent.replace(regex, match => '<mark>' + match + '</mark>');
-              node.parentNode.replaceChild(span, node);
-            });
-            
-            // Remove highlights after 5 seconds
-            setTimeout(() => {
-              const highlights = document.querySelectorAll('.search-term-highlight');
-              highlights.forEach(highlight => {
-                const text = highlight.textContent;
-                const textNode = document.createTextNode(text);
-                highlight.parentNode.replaceChild(textNode, highlight);
-              });
-            }, 5000);
-          }
-        }, 100); // Small delay to ensure content is rendered
-      }
-    });
+        }
+    }
   }
 
   // Check for stored line number and search term on page load
@@ -212,6 +216,17 @@ if (searchInput && searchResults) {
     }, 100);
   });
 
+  // Check for line number in URL hash on page load
+  window.addEventListener('load', () => {
+    const hash = window.location.hash;
+    if (hash.startsWith('#L')) {
+        const lineNumber = parseInt(hash.substring(2));
+        if (!isNaN(lineNumber)) {
+            scrollToLine(lineNumber);
+        }
+    }
+  });
+
   // Close search when clicking outside or pressing Escape
   document.addEventListener('click', (e) => {
     if (e.target === searchOverlay) {
@@ -260,6 +275,21 @@ fs.readdirSync(AGDA_HTML_DIR).forEach(file => {
              <link href="https://fonts.googleapis.com/css2?family=Fira+Code:wght@400;500&display=swap" rel="stylesheet">`
         );
 
+        // Wrap each line in the Agda content with a numbered div
+        content = content.replace(
+            /<pre class="Agda">([\s\S]*?)<\/pre>/g,
+            (match, content) => {
+                const lines = content.split('\n');
+                const numberedLines = lines.map(line => {
+                    if (line.trim() === '') {
+                        return '<div class="line"></div>';
+                    }
+                    return `<div class="line">${line}</div>`;
+                }).join('\n');
+                return `<pre class="Agda">${numberedLines}</pre>`;
+            }
+        );
+
         // Add header, sidebar, and theme toggle
         content = content.replace(
             /<body[^>]*>/,