js: fix @imkiva's reviews

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

@@ -1,16 +1,18 @@
-// Copyright 2023, Andreas Abel.
-// Falls under the Agda license at https://github.com/agda/agda/blob/master/LICENSE
+/*
+ * 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.
+ */
 
 // 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() {
+function highlightFn(root) {
   // Get all 'a' tags with an 'href' attribute.
   // We call those "objects".
-  const objs = document.querySelectorAll('a[href]');
+  const objs = root.querySelectorAll('a[href]');
 
   // Build a dictionary mapping a href to a set of objects that have this href.
   for (const obj of objs) {

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.
  */
 
-highlightFn();
+highlightFn(document);

pretty/src/main/resources/aya-html/show-tooltip-fn.js

@@ -110,7 +110,7 @@ class HoverStack {
     newHover.classList.add("AyaTooltipPopup");
     // Hover to highlight occurrences is done by adding mouse event listeners to the elements in the tooltip.
     // The inserted tooltip is not a child of `document` when the page was loaded, so a manual setup is needed.
-    setupHighlight(newHover);
+    highlightFn(newHover);
 
     // Auto-dismissal setup
     let self = this;