merge: #1019, deal with doc

Doc

.github/README.md

@@ -1,4 +1,4 @@
-[![actions]](https://github.com/aya-prover/aya-dev/actions/workflows/gradle-check.yml)
+[![actions]](https://github.com/aya-prover/aya-dev/actions/workflows/gradle-check.yaml)
 [![maven]][maven-repo]
 [![gitter]](https://gitter.im/aya-prover/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge)
 [![codecov]](https://codecov.io/gh/aya-prover/aya-dev)
@@ -66,7 +66,7 @@ of IDE is IntelliJ IDEA, version 2023.2 or higher is required.
     We value your time and enthusiasm, so we don't want to close your PRs :)
 
 [@ice1000]: https://github.com/ice1000
-[actions]: https://github.com/aya-prover/aya-dev/actions/workflows/gradle-check.yml/badge.svg
+[actions]: https://github.com/aya-prover/aya-dev/actions/workflows/gradle-check.yaml/badge.svg
 [codecov]: https://img.shields.io/codecov/c/github/aya-prover/aya-dev?logo=codecov&logoColor=white
 [gitter]: https://img.shields.io/gitter/room/aya-prover/community?color=cyan&logo=gitter
 [maven]: https://img.shields.io/maven-central/v/org.aya-prover/base?logo=gradle

base/src/test/java/org/aya/concrete/ParseTest.java

@@ -24,8 +24,7 @@
 import org.junit.jupiter.api.BeforeAll;
 import org.junit.jupiter.api.Test;
 
-import static org.junit.jupiter.api.Assertions.assertEquals;
-import static org.junit.jupiter.api.Assertions.assertTrue;
+import static org.junit.jupiter.api.Assertions.*;
 
 @SuppressWarnings("UnknownLanguage")
 public class ParseTest {
@@ -176,15 +175,15 @@ private void parseImport(@Language("Aya") String code) {
   }
 
   private void parseOpen(@Language("Aya") String code) {
-    assertTrue(parseStmt(code).last() instanceof Command.Open s && !s.toDoc(AyaPrettierOptions.debug()).debugRender().isEmpty());
+    assertTrue(parseStmt(code).getLast() instanceof Command.Open s && !s.toDoc(AyaPrettierOptions.debug()).debugRender().isEmpty());
   }
 
   private void parseFn(@Language("Aya") String code) {
     assertTrue(parseDecl(code).getFirst() instanceof TeleDecl.FnDecl s && !s.toDoc(AyaPrettierOptions.debug()).debugRender().isEmpty());
   }
 
   private void parseData(@Language("Aya") String code) {
-    assertTrue(parseDecl(code).getFirst() instanceof TeleDecl.DataDecl);
+    assertInstanceOf(TeleDecl.DataDecl.class, parseDecl(code).getFirst());
   }
 
   @Test

base/src/test/java/org/aya/experiments/NormalizeHugeChurch.java

@@ -31,7 +31,7 @@ def mul (a b : Num) : Num => \\A f x => a A (b A f) x
       """);
     var state = new TyckState(res.component1());
     var decls = res.component2();
-    var last = ((FnDef) decls.last()).body.getLeftValue();
+    var last = ((FnDef) decls.getLast()).body.getLeftValue();
     println("Tyck: " + (System.currentTimeMillis() - startup));
     startup = System.currentTimeMillis();
     var nf = last.normalize(state, NormalizeMode.NF);

base/src/test/java/org/aya/literate/HighlighterTester.java

@@ -91,7 +91,7 @@ public HighlighterTester(@NotNull String sourceCode, @NotNull ImmutableSeq<Highl
 
   public void runTest() {
     var sortedActual = actual.view().distinct().sorted().toImmutableSeq().view();
-    if (sortedActual.last() instanceof HighlightInfo.Lit(var $, var kind) && kind == HighlightInfo.LitKind.Eol)
+    if (sortedActual.getLast() instanceof HighlightInfo.Lit(var $, var kind) && kind == HighlightInfo.LitKind.Eol)
       // Remove the last Eol
       sortedActual = sortedActual.dropLast(1);
     runTest(sortedActual.toImmutableSeq(), Seq.of(expected));

base/src/test/java/org/aya/repr/ShapeMatcherTest.java

@@ -111,7 +111,7 @@ public void matchPlus() {
 
   public @Nullable ShapeRecognition match(boolean should, @NotNull AyaShape shape, @Language("Aya") @NonNls @NotNull String code) {
     var def = TyckDeclTest.successTyckDecls(code).component2();
-    return check(ImmutableSeq.fill(def.size(), Tuple.of(should, shape)), def).firstOrNull();
+    return check(ImmutableSeq.fill(def.size(), Tuple.of(should, shape)), def).getFirstOrNull();
   }
 
   public @NotNull ImmutableSeq<ShapeRecognition> match(@NotNull ImmutableSeq<Tuple2<Boolean, AyaShape>> shouldBe, @Language("Aya") @NonNls @NotNull String code) {

base/src/test/java/org/aya/tyck/PatCCTest.java

@@ -63,7 +63,7 @@ def nm (e : CExp) (nmAcc e) : CExp
          nm (if u (nm (if v y z) h1) (nm (if w y z) h2)) h3
       """);
     var decls = res.component2();
-    var classified = testClassify(res.component1(), (FnDef) decls.last());
+    var classified = testClassify(res.component1(), (FnDef) decls.getLast());
     assertEquals(3, classified.size());
     classified.forEach(cls ->
       assertEquals(1, cls.cls().size()));

pretty/src/main/java/org/aya/pretty/doc/Doc.java

@@ -47,10 +47,6 @@ default boolean isEmpty() {
   @Override default @NotNull Doc toDoc() {
     return this;
   }
-  /** @return a seq with cats flattened */
-  default @NotNull SeqLike<Doc> asSeq() {
-    return Seq.of(this);
-  }
 
   //region Doc APIs
   default @NotNull String renderToString(@NotNull StringPrinterConfig<?> config) {
@@ -127,11 +123,7 @@ default boolean isEmpty() {
 
   /** The empty document; conceptually the unit of 'Cat' */
   enum Empty implements Doc {
-    INSTANCE;
-
-    @Override public @NotNull SeqLike<Doc> asSeq() {
-      return Seq.empty();
-    }
+    INSTANCE
   }
 
   /**
@@ -215,9 +207,6 @@ record FlatAlt(@NotNull Doc defaultDoc, @NotNull Doc preferWhenFlatten) implemen
    * Concatenation of two documents
    */
   record Cat(@NotNull ImmutableSeq<Doc> inner) implements Doc {
-    @Override public @NotNull SeqLike<Doc> asSeq() {
-      return inner.view().flatMap(Doc::asSeq);
-    }
   }
 
   record List(boolean isOrdered, @NotNull ImmutableSeq<Doc> items) implements Doc {
@@ -796,6 +785,9 @@ record PageWidth(@NotNull IntFunction<Doc> docBuilder) implements Doc {
 
   //endregion
   private static @NotNull Doc simpleCat(@NotNull SeqLike<@NotNull Doc> xs) {
-    return new Cat(xs.view().flatMap(Doc::asSeq).toImmutableArray());
+    var seq = xs.toImmutableSeq();
+    if (seq.isEmpty()) return empty();
+    if (seq.sizeEquals(1)) return seq.getFirst();
+    return new Cat(seq);
   }
 }

pretty/src/main/java/org/aya/pretty/error/PrettyError.java

@@ -121,7 +121,7 @@ void add(int currentLine, @NotNull Doc code) {
     }
 
     void add(@NotNull Doc code) {
-      lineDocs.append(Doc.plain(" ")); // cannot use `empty()` or `plain("")`
+      lineDocs.append(Doc.ONE_WS); // cannot use `empty()` or `plain("")`
       codeDocs.append(code);
     }
   }
@@ -260,7 +260,7 @@ private void renderHints(
       .skip(Math.max(startLine - 1 - showMore, 0))
       .limit(endLine - startLine + 1 + showMore)
       .map(line -> visualizeLine(config, line))
-      .collect(MutableList.factory());
+      .toList();
 
     final int minLineNo = Math.max(startLine - showMore, 1);
     final int maxLineNo = minLineNo + lines.size();

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

@@ -3,24 +3,39 @@
  * Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
  */
 
-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(root) {
+  // Get all 'a' tags with an 'href' attribute.
+  // We call those "objects".
+  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) {
+    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(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;