misc: more fixes ig?

aya-prover · Nov 23, 2023 · 6be83e9 · 6be83e9
1 parent 6d5ab52
commit 6be83e9
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 5 deletions.
diff --git a/base/src/test/java/org/aya/concrete/ParseTest.java b/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

diff --git a/pretty/src/main/java/org/aya/pretty/error/PrettyError.java b/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);
     }
   }