merge: Display emoji in Windows Terminal (#1117)

Using jline dumb terminal

cli-console/src/main/java/org/aya/cli/console/AnsiReporter.java

@@ -3,6 +3,7 @@
 package org.aya.cli.console;
 
 import org.aya.pretty.printer.PrinterConfig;
+import org.aya.repl.ReplUtil;
 import org.aya.util.error.SourcePos;
 import org.aya.util.prettier.PrettierOptions;
 import org.aya.util.reporter.Problem;
@@ -27,7 +28,11 @@ public record AnsiReporter(
 ) implements Reporter {
   @Contract(pure = true, value = "_, _, _ -> new")
   public static @NotNull AnsiReporter stdio(boolean unicode, @NotNull PrettierOptions options, @NotNull Problem.Severity minimum) {
-    // AnsiConsole.systemInstall();
+    if (unicode) try {
+      var out = ReplUtil.jlineDumbTerminalWriter();
+      return new AnsiReporter(true, () -> true, () -> options, minimum, out, out);
+    } catch (Exception _) {
+    }
     return new AnsiReporter(true, () -> unicode, () -> options, minimum,
       System.out::println, System.err::println);
   }

cli-console/src/main/java/org/aya/cli/plct/PLCTReport.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.cli.plct;
 
@@ -9,6 +9,7 @@
 import kala.tuple.Tuple2;
 import org.aya.cli.console.MainArgs;
 import org.aya.pretty.doc.Doc;
+import org.aya.repl.ReplUtil;
 import org.jetbrains.annotations.Nls;
 import org.jetbrains.annotations.NotNull;
 
@@ -21,6 +22,7 @@
 import java.net.http.HttpResponse;
 import java.time.LocalDate;
 import java.time.LocalDateTime;
+import java.util.function.Consumer;
 
 public final class PLCTReport {
   @NotNull
@@ -29,8 +31,17 @@ public final class PLCTReport {
     Tuple.of("Aya VSCode", "aya-prover/aya-vscode"),
     Tuple.of("Aya Intellij Plugin", "aya-prover/intellij-aya")
   );
-  public static final @NotNull @Nls String SHRUG = "\ud83e\udd37";
+  public static final @NotNull @Nls String SHRUG = "🤷";
   private final @NotNull HttpClient client = HttpClient.newBuilder().version(HttpClient.Version.HTTP_2).build();
+  private Consumer<String> out;
+
+  {
+    try {
+      out = ReplUtil.jlineDumbTerminalWriter();
+    } catch (Exception _) {
+      out = System.out::println;
+    }
+  }
 
   private Doc pullRequest(GsonClasses.PR i) {
     return Doc.sepNonEmpty(
@@ -52,15 +63,15 @@ private Doc pullRequest(GsonClasses.PR i) {
 
   public int run(@NotNull MainArgs.PlctAction args) throws Exception {
     if (!args.plctReport) {
-      System.out.println(SHRUG);
+      out.accept(SHRUG);
       return 1;
     }
     Doc markdown;
     LocalDateTime since;
     if (args.reportSince > 0) {
       since = LocalDate.now().minusDays(args.reportSince).atStartOfDay();
     } else if (args.reportSince < 0) {
-      System.out.println(SHRUG);
+      out.accept(SHRUG);
       return 1;
     } else since = sinceDate().atStartOfDay();
     if (args.repoName != null) {
@@ -71,7 +82,7 @@ public int run(@NotNull MainArgs.PlctAction args) throws Exception {
         .view()
         .prepended(Doc.plain("## The Aya Theorem Prover")));
     }
-    System.out.println(markdown.debugRender());
+    out.accept(markdown.debugRender());
     return 0;
   }
 
@@ -104,7 +115,7 @@ public int run(@NotNull MainArgs.PlctAction args) throws Exception {
       ? LocalDate.of(year, month, 1)
       // Generating the report at the start of next month -- collect last month
       : month == 1 ? LocalDate.of(year - 1, 12, 1)
-      : LocalDate.of(year, month - 1, 1);
+        : LocalDate.of(year, month - 1, 1);
   }
 
   public static @NotNull ImmutableSeq<GsonClasses.PR> parse(@NotNull InputStream input) {

cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.cli.single;
 
@@ -54,8 +54,8 @@ public record PrettyInfo(
   }
 
   public record Message(
-    @NotNull String successNotion,
-    @NotNull String failNotion
+    @NotNull String successNotation,
+    @NotNull String failNotation
   ) {
     public static final Message EMOJI = new Message("🎉", "🥲");
     public static final Message ASCII = new Message("That looks right!", "Let's learn from that.");

cli-impl/src/main/java/org/aya/cli/utils/CompilerUtil.java

@@ -36,11 +36,11 @@ public static int catching(
       if (flags.interruptedTrace()) e.printStackTrace();
     }
     if (reporter.noError()) {
-      reporter.reportString(flags.message().successNotion());
+      reporter.reportString(flags.message().successNotation());
       return 0;
     } else {
       reporter.reportString(reporter.countToString());
-      reporter.reportString(flags.message().failNotion());
+      reporter.reportString(flags.message().failNotation());
       return 1;
     }
   }

pretty/src/main/java/org/aya/pretty/backend/latex/DocTeXPrinter.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.pretty.backend.latex;
 
@@ -69,30 +69,30 @@ protected void renderStyleCommand(@NotNull Cursor cursor) {
     Tuple.of("/\\", "\\land"),
     Tuple.of("|", "\\mid"),
     Tuple.of("=>", "\\Rightarrow"),
-    Tuple.of("\u2191", "\\uparrow"),
+    Tuple.of("↑", "\\uparrow"),
     Tuple.of("->", "\\to"),
     Tuple.of("_|_", "\\bot"),
     Tuple.of("forall", "\\forall"),
-    Tuple.of("\u03A3", "\\Sigma"),
-    Tuple.of("\u2228", "\\lor"),
-    Tuple.of("\u2227", "\\land"),
-    Tuple.of("\u21D2", "\\Rightarrow"),
-    Tuple.of("\u2192", "\\to"),
-    Tuple.of("\u22A5", "\\bot"),
-    Tuple.of("\u2200", "\\forall"),
+    Tuple.of("Σ", "\\Sigma"),
+    Tuple.of("∨", "\\lor"),
+    Tuple.of("∧", "\\land"),
+    Tuple.of("⇒", "\\Rightarrow"),
+    Tuple.of("→", "\\to"),
+    Tuple.of("⊥", "\\bot"),
+    Tuple.of("∀", "\\forall"),
     Tuple.of("_", "\\_"),
     Tuple.of("~", "\\neg"),
     Tuple.of("**", "\\times"),
     id("(|"), id("|)"),
-    Tuple.of("\u2987", "(|"),
-    Tuple.of("\u2988", "|)"),
+    Tuple.of("⦇", "(|"),
+    Tuple.of("⦈", "|)"),
     id("[|"), id("|]"),
-    Tuple.of("\u27E6", "[|"),
-    Tuple.of("\u27E7", "|]"),
+    Tuple.of("⟦", "[|"),
+    Tuple.of("⟧", "|]"),
     Tuple.of("{|", "\\{|"),
     Tuple.of("|}", "|\\}"),
-    Tuple.of("\u2983", "\\{|"),
-    Tuple.of("\u2984", "|\\}"),
+    Tuple.of("⦃", "\\{|"),
+    Tuple.of("⦄", "|\\}"),
     id(":"), id("."), id(":="), id("="),
     id("("), id(")"),
     Tuple.of("{", "\\{"),

pretty/src/main/java/org/aya/pretty/backend/md/DocMdPrinter.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.pretty.backend.md;
 
@@ -19,8 +19,7 @@ public class DocMdPrinter extends DocHtmlPrinter<DocMdPrinter.Config> {
   /** `Doc.plain("1. hello")` should not be rendered as a list, see MdStyleTest */
   public static final Pattern MD_ESCAPE_FAKE_LIST = Pattern.compile("(^\\s*\\d+)\\.( |$)", Pattern.MULTILINE);
 
-  @Override protected void renderHeader(@NotNull Cursor cursor) {
-  }
+  @Override protected void renderHeader(@NotNull Cursor cursor) { }
 
   @Override protected void renderFooter(@NotNull Cursor cursor) {
     // put generated styles at the end of the file

pretty/src/main/java/org/aya/pretty/backend/md/MdStyle.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.pretty.backend.md;
 
@@ -15,5 +15,5 @@ enum GFM implements MdStyle {
     return new Heading(level);
   }
 
-  record Heading(int level) implements MdStyle {}
+  record Heading(int level) implements MdStyle { }
 }

pretty/src/main/java/org/aya/pretty/backend/string/ClosingStylist.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.pretty.backend.string;
 
@@ -23,7 +23,7 @@ public StyleToken(@NotNull String start, @NotNull String end, boolean visible) {
       this(c -> c.content(start, visible), c -> c.content(end, visible));
     }
 
-    public static final @NotNull StyleToken NULL = new StyleToken(c -> {}, c -> {});
+    public static final @NotNull StyleToken NULL = new StyleToken(_ -> { }, _ -> { });
   }
 
   @Override
@@ -110,7 +110,7 @@ public Delegate(@NotNull ClosingStylist delegate) {
 
     @Override
     protected @NotNull StyleToken formatLineThrough(@NotNull Style.LineThrough line, EnumSet<StringPrinter.Outer> outer) {
-      return delegate.formatLineThrough(line,outer);
+      return delegate.formatLineThrough(line, outer);
     }
 
     @Override protected @NotNull StyleToken formatColorHex(int rgb, boolean background) {

pretty/src/main/java/org/aya/pretty/backend/string/Cursor.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.pretty.backend.string;
 
@@ -11,21 +11,10 @@ public class Cursor {
   private final StringBuilder builder = new StringBuilder();
   private final StringPrinter<?> printer;
 
-  public Cursor(StringPrinter<?> printer) {
-    this.printer = printer;
-  }
-
-  public @NotNull CharSequence result() {
-    return builder;
-  }
-
-  public int getCursor() {
-    return cursor;
-  }
-
-  public int getNestLevel() {
-    return nestLevel;
-  }
+  public Cursor(StringPrinter<?> printer) { this.printer = printer; }
+  public @NotNull CharSequence result() { return builder; }
+  public int getCursor() { return cursor; }
+  public int getNestLevel() { return nestLevel; }
 
   public void content(@NotNull CharSequence content, boolean visible) {
     if (visible) visibleContent(content);
@@ -58,19 +47,9 @@ public void lineBreakWith(@NotNull CharSequence lineBreak) {
     invisibleContent(lineBreak);
     moveToNewLine();
   }
-
-  public boolean isAtLineStart() {
-    return cursor == lineStartCursor;
-  }
-
-  public void moveToNewLine() {
-    cursor = lineStartCursor = 0;
-  }
-
-  public void moveForward(int count) {
-    cursor += Math.max(0, count);
-  }
-
+  public boolean isAtLineStart() { return cursor == lineStartCursor; }
+  public void moveToNewLine() { cursor = lineStartCursor = 0; }
+  public void moveForward(int count) { cursor += Math.max(0, count); }
   public void nested(int nest, @NotNull Runnable r) {
     nestLevel += nest;
     r.run();