html: update js to the one from Agda

pretty/src/main/resources/aya-html/highlight-fn.js

@@ -1,26 +1,39 @@
-/*
- * Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
- * Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
- */
+// Copyright 2023, Andreas Abel.
+// Falls under the Agda license at https://github.com/agda/agda/blob/master/LICENSE
 
-function highlight(on) {
-  return function () {
-    let links = document.getElementsByTagName('a');
-    for (let i = 0; i < links.length; i++) {
-      let that = links[i];
-      if (this.href !== that.href) continue;
-      if (on) that.classList.add("hover-highlight");
-      else that.classList.remove("hover-highlight");
-    }
+// When we hover over an Agda identifier, we highlight all occurrences of this identifier on the page.
+// To this end, we create a map from identifier to all of its occurrences in the beginning.
+
+// A dictionary from hrefs to 'a'-elements that have this href.
+const dict = new Map();
+
+function highlightFn() {
+  // Get all 'a' tags with an 'href' attribute.
+  // We call those "objects".
+  const objs = document.querySelectorAll('a[href]');
+
+  // Build a dictionary mapping a href to a set of objects that have this href.
+  for (const obj of objs) {
+    const key = obj.href;
+    const set = dict.get(key) ?? new Set();
+    set.add(obj);
+    dict.set(key, set);
   }
-}
 
-function setupHighlight(dom) {
-  let links = dom.getElementsByTagName('a');
-  for (let i = 0; i < links.length; i++) {
-    let link = links[i];
-    if (!link.hasAttribute("href")) continue;
-    link.onmouseover = highlight(true);
-    link.onmouseout = highlight(false);
+  // Install 'onmouseover' and 'onmouseout' event handlers for all objects.
+  for (const obj of objs) {
+    // 'onmouseover' for an object adds attribute 'hover-highlight' to all objects with the same href.
+    obj.onmouseover = function () {
+      for (const o of dict.get(this.href)) {
+        o.classList.add('hover-highlight');
+      }
+    }
+    // 'onmouseover' removes the added 'hover-highlight' attributes again.
+    obj.onmouseout = function () {
+      for (const o of dict.get(this.href)) {
+        o.classList.remove('hover-highlight');
+      }
+    }
   }
 }
+

pretty/src/main/resources/aya-html/highlight-occurrences.js

@@ -3,4 +3,4 @@
  * Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
  */
 
-setupHighlight(document);
+highlightFn();