util: extract

aya-prover · Jun 19, 2024 · 3aa4ae4 · 3aa4ae4
1 parent bb295cc
commit 3aa4ae4
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 10 deletions.
diff --git a/cli-console/src/main/java/org/aya/cli/console/AnsiReporter.java b/cli-console/src/main/java/org/aya/cli/console/AnsiReporter.java
@@ -3,13 +3,13 @@
 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;
 import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
-import org.jline.terminal.TerminalBuilder;
 
 import java.util.function.BooleanSupplier;
 import java.util.function.Consumer;
@@ -29,11 +29,7 @@ public record AnsiReporter(
   @Contract(pure = true, value = "_, _, _ -> new")
   public static @NotNull AnsiReporter stdio(boolean unicode, @NotNull PrettierOptions options, @NotNull Problem.Severity minimum) {
     if (unicode) try {
-      var terminal = TerminalBuilder.builder().jni(true).dumb(true).build();
-      Consumer<String> out = s -> {
-        terminal.writer().println(s);
-        terminal.flush();
-      };
+      var out = ReplUtil.jlineDumbTerminalWriter();
       return new AnsiReporter(true, () -> true, () -> options, minimum, out, out);
     } catch (Exception _) {
     }

diff --git a/cli-console/src/main/java/org/aya/cli/plct/PLCTReport.java b/cli-console/src/main/java/org/aya/cli/plct/PLCTReport.java
@@ -9,9 +9,9 @@
 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;
-import org.jline.terminal.TerminalBuilder;
 
 import java.io.IOException;
 import java.io.InputStream;
@@ -37,8 +37,7 @@ public final class PLCTReport {
 
   {
     try {
-      var terminal = TerminalBuilder.builder().jni(true).dumb(true).build();
-      out = s -> terminal.writer().println(s);
+      out = ReplUtil.jlineDumbTerminalWriter();
     } catch (Exception _) {
       out = System.out::println;
     }

diff --git a/tools-repl/src/main/java/org/aya/repl/ReplUtil.java b/tools-repl/src/main/java/org/aya/repl/ReplUtil.java
@@ -1,14 +1,17 @@
-// 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.repl;
 
 import org.aya.pretty.doc.Doc;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
+import org.jline.terminal.TerminalBuilder;
 import org.jline.utils.AttributedStringBuilder;
 import org.jline.utils.AttributedStyle;
 
+import java.io.IOException;
 import java.nio.file.Path;
+import java.util.function.Consumer;
 
 public interface ReplUtil {
   static @NotNull Command.Result invokeHelp(CommandManager commandManager, @Nullable HelpItem argument) {
@@ -43,4 +46,12 @@ record HelpItem(@NotNull String cmd) {
       .style(AttributedStyle.DEFAULT)
       .toAnsi();
   }
+
+  static @NotNull Consumer<String> jlineDumbTerminalWriter() throws IOException {
+    var terminal = TerminalBuilder.builder().jni(true).dumb(true).build();
+    return s -> {
+      terminal.writer().println(s);
+      terminal.flush();
+    };
+  }
 }