TEST: test stderr output

aya-prover · Nov 4, 2021 · 85e6a08 · 85e6a08
1 parent 7d9305f
commit 85e6a08
Show file tree

Hide file tree

Showing 4 changed files with 33 additions and 15 deletions.
diff --git a/cli/src/main/java/org/aya/cli/repl/Repl.java b/cli/src/main/java/org/aya/cli/repl/Repl.java
@@ -158,19 +158,22 @@ private boolean singleLoop() {
   public static class PlainRepl extends Repl {
     private final @NotNull Scanner scanner;
     private final @NotNull PrintWriter out;
+    private final @NotNull PrintWriter err;
 
     public PlainRepl(@NotNull ReplConfig config) {
-      this(config, new InputStreamReader(System.in), new PrintWriter(System.out));
+      this(config, new InputStreamReader(System.in), new PrintWriter(System.out), new PrintWriter(System.err));
     }
 
     public PlainRepl(
       @NotNull ReplConfig config,
       @NotNull Readable input,
-      @NotNull Writer out
+      @NotNull Writer out,
+      @NotNull Writer err
     ) {
       super(config);
       scanner = new Scanner(input);
       this.out = new PrintWriter(out);
+      this.err = new PrintWriter(err);
     }
 
     @Override protected @NotNull String readLine(@NotNull String prompt) {
@@ -184,7 +187,7 @@ public PlainRepl(
     }
 
     @Override protected void errPrintln(@NotNull String x) {
-      System.err.println(x);
+      err.println(x);
     }
 
     @Override protected @Nullable String hintMessage() {

diff --git a/cli/src/main/java/org/aya/cli/repl/jline/JlineRepl.java b/cli/src/main/java/org/aya/cli/repl/jline/JlineRepl.java
@@ -10,6 +10,7 @@
 import org.aya.pretty.doc.Doc;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
+import org.jetbrains.annotations.VisibleForTesting;
 import org.jline.reader.EndOfFileException;
 import org.jline.reader.LineReader;
 import org.jline.reader.LineReaderBuilder;
@@ -29,7 +30,8 @@
 
 public final class JlineRepl extends Repl {
   private final @NotNull Terminal terminal;
-  private final @NotNull LineReader lineReader;
+  @VisibleForTesting
+  public final @NotNull LineReader lineReader;
 
   public JlineRepl(@NotNull ReplConfig config) throws IOException {
     super(config);

diff --git a/cli/src/test/java/org/aya/cli/JlineReplTest.java b/cli/src/test/java/org/aya/cli/JlineReplTest.java
@@ -58,7 +58,7 @@ public class JlineReplTest {
   @Test public void parenTyCode() {
     var line = parser.parse("(Ty", 2);
     var candidates = new ArrayList<Candidate>();
-    AyaCompleters.KW.complete(null, line, candidates);
+    AyaCompleters.KW.complete(repl.lineReader, line, candidates);
     assertFalse(candidates.isEmpty());
   }
 

diff --git a/cli/src/test/java/org/aya/cli/PlainReplTest.java b/cli/src/test/java/org/aya/cli/PlainReplTest.java
@@ -2,6 +2,8 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.cli;
 
+import kala.tuple.Tuple;
+import kala.tuple.Tuple2;
 import org.aya.cli.repl.Repl;
 import org.aya.cli.repl.ReplConfig;
 import org.jetbrains.annotations.NotNull;
@@ -29,7 +31,7 @@ public class PlainReplTest {
   }
 
   @Test public void help() {
-    var repl = repl(":help");
+    var repl = repl(":help")._1;
     assertTrue(repl.contains("help"));
     assertTrue(repl.contains("REPL"));
   }
@@ -43,32 +45,43 @@ public class PlainReplTest {
   }
 
   @Test public void typeType() {
-    assertTrue(repl(":type Type").contains("Type"));
+    assertTrue(repl(":type Type")._1.contains("Type"));
   }
 
   @Test public void amb() {
-    assertTrue(repl(":p").contains("Ambiguous"));
+    assertTrue(repl(":p")._2.contains("Ambiguous"));
+  }
+
+  @Test public void notFound() {
+    assertTrue(repl(":cthulhu")._2.contains("not found"));
   }
 
   @Test public void type() {
-    assertTrue(repl("Type").contains("Type"));
+    assertTrue(repl("Type")._1.contains("Type"));
+  }
+
+  @Test public void disableUnicode() {
+    assertTrue(repl(":unicode no")._1.contains("disable"));
+    assertTrue(repl(":unicode yes")._1.contains("enable"));
+    assertTrue(repl(":unicode false")._1.contains("disable"));
   }
 
   @Test public void pwd() {
-    assertTrue(repl(":pwd").contains("aya"));
+    assertTrue(repl(":pwd")._1.contains("aya"));
   }
 
   @Test public void typeSuc() {
-    var repl = repl("data Nat : Type | suc Nat | zero\n:type Nat::suc");
+    var repl = repl("data Nat : Type | suc Nat | zero\n:type Nat::suc")._1;
     assertTrue(repl.contains("Nat"));
     assertTrue(repl.contains("->"));
   }
 
-  private @NotNull String repl(@NotNull String input) {
-    var writer = new StringWriter();
+  private @NotNull Tuple2<String, String> repl(@NotNull String input) {
+    var out = new StringWriter();
+    var err = new StringWriter();
     var reader = new StringReader(input + "\n:exit");
-    var repl = new Repl.PlainRepl(config, reader, writer);
+    var repl = new Repl.PlainRepl(config, reader, out, err);
     repl.run();
-    return writer.toString();
+    return Tuple.of(out.toString(), err.toString());
   }
 }