From c821c002c61758b66fde66485f144b5325ed0f23 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Wed, 19 Jun 2024 16:51:46 -0400 Subject: [PATCH 1/4] stdio: use `System.console` --- base/src/test/java/org/aya/tyck/TyckTest.java | 5 +++-- .../java/org/aya/cli/console/AnsiReporter.java | 5 ++++- .../src/main/java/org/aya/cli/console/Main.java | 2 +- .../main/java/org/aya/cli/plct/PLCTReport.java | 8 ++++---- .../java/org/aya/cli/single/CompilerFlags.java | 6 +++--- .../java/org/aya/cli/utils/CompilerUtil.java | 4 ++-- .../java/org/aya/util/reporter/Reporter.java | 16 ++++------------ 7 files changed, 21 insertions(+), 25 deletions(-) diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java index 0f338a872e..a16af2155f 100644 --- a/base/src/test/java/org/aya/tyck/TyckTest.java +++ b/base/src/test/java/org/aya/tyck/TyckTest.java @@ -197,8 +197,9 @@ class Monoid var endTime = System.currentTimeMillis(); assertNotNull(sortResult); - System.out.println(STR."Done in \{(endTime - beginTime)}"); - System.out.println(sortResult.debuggerOnlyToString()); + var writer = System.console().writer(); + writer.println(STR."Done in \{(endTime - beginTime)}"); + writer.println(sortResult.debuggerOnlyToString()); } public record TyckResult(@NotNull ImmutableSeq defs, @NotNull ResolveInfo info) { } 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 index e11c7701ff..d79a6d0fbc 100644 --- a/cli-console/src/main/java/org/aya/cli/console/AnsiReporter.java +++ b/cli-console/src/main/java/org/aya/cli/console/AnsiReporter.java @@ -29,7 +29,10 @@ public record AnsiReporter( public static @NotNull AnsiReporter stdio(boolean unicode, @NotNull PrettierOptions options, @NotNull Problem.Severity minimum) { // AnsiConsole.systemInstall(); return new AnsiReporter(true, () -> unicode, () -> options, minimum, - System.out::println, System.err::println); + s -> { + System.console().writer().println(s); + System.console().flush(); + }, System.err::println); } @Override public void report(@NotNull Problem problem) { diff --git a/cli-console/src/main/java/org/aya/cli/console/Main.java b/cli-console/src/main/java/org/aya/cli/console/Main.java index 221626beac..f1f25cec21 100644 --- a/cli-console/src/main/java/org/aya/cli/console/Main.java +++ b/cli-console/src/main/java/org/aya/cli/console/Main.java @@ -70,7 +70,7 @@ private int doFakeLiterate() throws IOException { var setup = info.backendOpts(false); var output = renderOptions.render(prettyFormat.target, doc, setup); if (outputPath != null) FileUtil.writeString(outputPath, output); - else System.out.println(output); + else System.console().writer().write(output); return 0; } 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 index ade3c449d1..7762f51904 100644 --- a/cli-console/src/main/java/org/aya/cli/plct/PLCTReport.java +++ b/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; @@ -52,7 +52,7 @@ private Doc pullRequest(GsonClasses.PR i) { public int run(@NotNull MainArgs.PlctAction args) throws Exception { if (!args.plctReport) { - System.out.println(SHRUG); + System.console().writer().println(SHRUG); return 1; } Doc markdown; @@ -60,7 +60,7 @@ public int run(@NotNull MainArgs.PlctAction args) throws Exception { if (args.reportSince > 0) { since = LocalDate.now().minusDays(args.reportSince).atStartOfDay(); } else if (args.reportSince < 0) { - System.out.println(SHRUG); + System.console().writer().println(SHRUG); return 1; } else since = sinceDate().atStartOfDay(); if (args.repoName != null) { @@ -71,7 +71,7 @@ public int run(@NotNull MainArgs.PlctAction args) throws Exception { .view() .prepended(Doc.plain("## The Aya Theorem Prover"))); } - System.out.println(markdown.debugRender()); + System.console().writer().println(markdown.debugRender()); return 0; } diff --git a/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java b/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java index 1aa21ed522..91e0d59753 100644 --- a/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java +++ b/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."); diff --git a/cli-impl/src/main/java/org/aya/cli/utils/CompilerUtil.java b/cli-impl/src/main/java/org/aya/cli/utils/CompilerUtil.java index 1a14baca85..11f16086f6 100644 --- a/cli-impl/src/main/java/org/aya/cli/utils/CompilerUtil.java +++ b/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; } } diff --git a/tools/src/main/java/org/aya/util/reporter/Reporter.java b/tools/src/main/java/org/aya/util/reporter/Reporter.java index 6bb9e5679a..1fd98d31e5 100644 --- a/tools/src/main/java/org/aya/util/reporter/Reporter.java +++ b/tools/src/main/java/org/aya/util/reporter/Reporter.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.util.reporter; @@ -44,17 +44,9 @@ default void reportDoc(@NotNull Doc doc, final Problem.Severity severity) { static @NotNull Problem dummyProblem(@NotNull Doc doc, Problem.Severity severity) { return new Problem() { - @Override public @NotNull SourcePos sourcePos() { - return SourcePos.NONE; - } - - @Override public @NotNull Severity level() { - return severity; - } - - @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { - return doc; - } + @Override public @NotNull SourcePos sourcePos() { return SourcePos.NONE; } + @Override public @NotNull Severity level() { return severity; } + @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { return doc; } }; } From bb295cc9201362d50b5f30598b1a2d5a9d8c79ba Mon Sep 17 00:00:00 2001 From: ice1000 Date: Wed, 19 Jun 2024 16:53:44 -0400 Subject: [PATCH 2/4] stdio: use jline dumb terminal --- base/src/test/java/org/aya/tyck/TyckTest.java | 5 ++--- .../org/aya/cli/console/AnsiReporter.java | 16 ++++++++++----- .../main/java/org/aya/cli/console/Main.java | 2 +- .../java/org/aya/cli/plct/PLCTReport.java | 20 +++++++++++++++---- .../org/aya/cli/single/CompilerFlags.java | 2 +- 5 files changed, 31 insertions(+), 14 deletions(-) diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java index a16af2155f..0f338a872e 100644 --- a/base/src/test/java/org/aya/tyck/TyckTest.java +++ b/base/src/test/java/org/aya/tyck/TyckTest.java @@ -197,9 +197,8 @@ class Monoid var endTime = System.currentTimeMillis(); assertNotNull(sortResult); - var writer = System.console().writer(); - writer.println(STR."Done in \{(endTime - beginTime)}"); - writer.println(sortResult.debuggerOnlyToString()); + System.out.println(STR."Done in \{(endTime - beginTime)}"); + System.out.println(sortResult.debuggerOnlyToString()); } public record TyckResult(@NotNull ImmutableSeq defs, @NotNull ResolveInfo info) { } 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 index d79a6d0fbc..21e5277b99 100644 --- a/cli-console/src/main/java/org/aya/cli/console/AnsiReporter.java +++ b/cli-console/src/main/java/org/aya/cli/console/AnsiReporter.java @@ -9,6 +9,7 @@ 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; @@ -27,12 +28,17 @@ 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 terminal = TerminalBuilder.builder().jni(true).dumb(true).build(); + Consumer out = s -> { + terminal.writer().println(s); + terminal.flush(); + }; + return new AnsiReporter(true, () -> true, () -> options, minimum, out, out); + } catch (Exception _) { + } return new AnsiReporter(true, () -> unicode, () -> options, minimum, - s -> { - System.console().writer().println(s); - System.console().flush(); - }, System.err::println); + System.out::println, System.err::println); } @Override public void report(@NotNull Problem problem) { diff --git a/cli-console/src/main/java/org/aya/cli/console/Main.java b/cli-console/src/main/java/org/aya/cli/console/Main.java index f1f25cec21..221626beac 100644 --- a/cli-console/src/main/java/org/aya/cli/console/Main.java +++ b/cli-console/src/main/java/org/aya/cli/console/Main.java @@ -70,7 +70,7 @@ private int doFakeLiterate() throws IOException { var setup = info.backendOpts(false); var output = renderOptions.render(prettyFormat.target, doc, setup); if (outputPath != null) FileUtil.writeString(outputPath, output); - else System.console().writer().write(output); + else System.out.println(output); return 0; } 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 index 7762f51904..f40e76ad7d 100644 --- a/cli-console/src/main/java/org/aya/cli/plct/PLCTReport.java +++ b/cli-console/src/main/java/org/aya/cli/plct/PLCTReport.java @@ -11,6 +11,7 @@ import org.aya.pretty.doc.Doc; import org.jetbrains.annotations.Nls; import org.jetbrains.annotations.NotNull; +import org.jline.terminal.TerminalBuilder; import java.io.IOException; import java.io.InputStream; @@ -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 @@ -31,6 +33,16 @@ public final class PLCTReport { ); public static final @NotNull @Nls String SHRUG = "\ud83e\udd37"; private final @NotNull HttpClient client = HttpClient.newBuilder().version(HttpClient.Version.HTTP_2).build(); + private Consumer out; + + { + try { + var terminal = TerminalBuilder.builder().jni(true).dumb(true).build(); + out = s -> terminal.writer().println(s); + } catch (Exception _) { + out = System.out::println; + } + } private Doc pullRequest(GsonClasses.PR i) { return Doc.sepNonEmpty( @@ -52,7 +64,7 @@ private Doc pullRequest(GsonClasses.PR i) { public int run(@NotNull MainArgs.PlctAction args) throws Exception { if (!args.plctReport) { - System.console().writer().println(SHRUG); + out.accept(SHRUG); return 1; } Doc markdown; @@ -60,7 +72,7 @@ public int run(@NotNull MainArgs.PlctAction args) throws Exception { if (args.reportSince > 0) { since = LocalDate.now().minusDays(args.reportSince).atStartOfDay(); } else if (args.reportSince < 0) { - System.console().writer().println(SHRUG); + out.accept(SHRUG); return 1; } else since = sinceDate().atStartOfDay(); if (args.repoName != null) { @@ -71,7 +83,7 @@ public int run(@NotNull MainArgs.PlctAction args) throws Exception { .view() .prepended(Doc.plain("## The Aya Theorem Prover"))); } - System.console().writer().println(markdown.debugRender()); + out.accept(markdown.debugRender()); return 0; } @@ -104,7 +116,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 parse(@NotNull InputStream input) { diff --git a/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java b/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java index 91e0d59753..8e2a649113 100644 --- a/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java +++ b/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java @@ -57,7 +57,7 @@ public record Message( @NotNull String successNotation, @NotNull String failNotation ) { - public static final Message EMOJI = new Message("🎉", "🥲"); + public static final Message EMOJI = new Message("\uD83C\uDF89", "\uD83E\uDD72"); public static final Message ASCII = new Message("That looks right!", "Let's learn from that."); } } From 3aa4ae499085d54185425d3ad36bf31d0a4d28f9 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Wed, 19 Jun 2024 16:49:03 -0400 Subject: [PATCH 3/4] util: extract --- .../main/java/org/aya/cli/console/AnsiReporter.java | 8 ++------ .../src/main/java/org/aya/cli/plct/PLCTReport.java | 5 ++--- tools-repl/src/main/java/org/aya/repl/ReplUtil.java | 13 ++++++++++++- 3 files changed, 16 insertions(+), 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 index 21e5277b99..d9e8b5efa9 100644 --- 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 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 index f40e76ad7d..0b92ebc009 100644 --- 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 index aab968c5d4..f208680f62 100644 --- 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 jlineDumbTerminalWriter() throws IOException { + var terminal = TerminalBuilder.builder().jni(true).dumb(true).build(); + return s -> { + terminal.writer().println(s); + terminal.flush(); + }; + } } From ce075408d5329ebcaf2af59922bc5d0d58abc371 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Wed, 19 Jun 2024 17:13:50 -0400 Subject: [PATCH 4/4] pretty: use unicode literal in the code --- .../java/org/aya/cli/plct/PLCTReport.java | 2 +- .../org/aya/cli/single/CompilerFlags.java | 2 +- .../pretty/backend/latex/DocTeXPrinter.java | 30 +++++----- .../aya/pretty/backend/md/DocMdPrinter.java | 5 +- .../org/aya/pretty/backend/md/MdStyle.java | 4 +- .../pretty/backend/string/ClosingStylist.java | 6 +- .../org/aya/pretty/backend/string/Cursor.java | 37 +++---------- .../pretty/backend/string/StringPrinter.java | 55 ++++++++----------- .../pretty/backend/string/StringStylist.java | 9 ++- 9 files changed, 62 insertions(+), 88 deletions(-) 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 index 0b92ebc009..3a79b3d80e 100644 --- a/cli-console/src/main/java/org/aya/cli/plct/PLCTReport.java +++ b/cli-console/src/main/java/org/aya/cli/plct/PLCTReport.java @@ -31,7 +31,7 @@ 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 out; diff --git a/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java b/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java index 8e2a649113..91e0d59753 100644 --- a/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java +++ b/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java @@ -57,7 +57,7 @@ public record Message( @NotNull String successNotation, @NotNull String failNotation ) { - public static final Message EMOJI = new Message("\uD83C\uDF89", "\uD83E\uDD72"); + public static final Message EMOJI = new Message("🎉", "🥲"); public static final Message ASCII = new Message("That looks right!", "Let's learn from that."); } } diff --git a/pretty/src/main/java/org/aya/pretty/backend/latex/DocTeXPrinter.java b/pretty/src/main/java/org/aya/pretty/backend/latex/DocTeXPrinter.java index fce3760a7b..a43d7915ee 100644 --- a/pretty/src/main/java/org/aya/pretty/backend/latex/DocTeXPrinter.java +++ b/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("{", "\\{"), diff --git a/pretty/src/main/java/org/aya/pretty/backend/md/DocMdPrinter.java b/pretty/src/main/java/org/aya/pretty/backend/md/DocMdPrinter.java index 66498ead60..0f579325f9 100644 --- a/pretty/src/main/java/org/aya/pretty/backend/md/DocMdPrinter.java +++ b/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 { /** `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 diff --git a/pretty/src/main/java/org/aya/pretty/backend/md/MdStyle.java b/pretty/src/main/java/org/aya/pretty/backend/md/MdStyle.java index 8fe83f2908..c81cebe364 100644 --- a/pretty/src/main/java/org/aya/pretty/backend/md/MdStyle.java +++ b/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 { } } diff --git a/pretty/src/main/java/org/aya/pretty/backend/string/ClosingStylist.java b/pretty/src/main/java/org/aya/pretty/backend/string/ClosingStylist.java index fd678ec287..09fd5f78b7 100644 --- a/pretty/src/main/java/org/aya/pretty/backend/string/ClosingStylist.java +++ b/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 outer) { - return delegate.formatLineThrough(line,outer); + return delegate.formatLineThrough(line, outer); } @Override protected @NotNull StyleToken formatColorHex(int rgb, boolean background) { diff --git a/pretty/src/main/java/org/aya/pretty/backend/string/Cursor.java b/pretty/src/main/java/org/aya/pretty/backend/string/Cursor.java index 1ed4c10d70..239c31e64a 100644 --- a/pretty/src/main/java/org/aya/pretty/backend/string/Cursor.java +++ b/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(); diff --git a/pretty/src/main/java/org/aya/pretty/backend/string/StringPrinter.java b/pretty/src/main/java/org/aya/pretty/backend/string/StringPrinter.java index 5eec6eab13..6a6fd6b548 100644 --- a/pretty/src/main/java/org/aya/pretty/backend/string/StringPrinter.java +++ b/pretty/src/main/java/org/aya/pretty/backend/string/StringPrinter.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; @@ -52,7 +52,7 @@ private int lineRemaining(@NotNull Cursor cursor) { protected int predictWidth(@NotNull Cursor cursor, @NotNull Doc doc) { return switch (doc) { - case Doc.Empty d -> 0; + case Doc.Empty _, Doc.Line _ -> 0; case Doc.PlainText(var text) -> text.length(); case Doc.EscapedText(var text) -> text.length(); case Doc.SpecialSymbol(var text) -> text.length(); @@ -60,7 +60,6 @@ protected int predictWidth(@NotNull Cursor cursor, @NotNull Doc doc) { case Doc.Image i -> predictWidth(cursor, i.alt()); case Doc.Styled styled -> predictWidth(cursor, styled.doc()); case Doc.Tooltip tooltip -> predictWidth(cursor, tooltip.doc()); - case Doc.Line d -> 0; case Doc.FlatAlt alt -> predictWidth(cursor, alt.defaultDoc()); case Doc.Cat cat -> cat.inner().view().map(inner -> predictWidth(cursor, inner)).reduce(Integer::sum); case Doc.Nest nest -> predictWidth(cursor, nest.doc()) + nest.indent(); @@ -84,11 +83,8 @@ protected int predictWidth(@NotNull Cursor cursor, @NotNull Doc doc) { return lineRem == PrinterConfig.INFINITE_SIZE || predictWidth(cursor, a) <= lineRem ? a : b; } - protected void renderHeader(@NotNull Cursor cursor) { - } - - protected void renderFooter(@NotNull Cursor cursor) { - } + protected void renderHeader(@NotNull Cursor cursor) { } + protected void renderFooter(@NotNull Cursor cursor) { } protected void renderDoc(@NotNull Cursor cursor, @NotNull Doc doc, EnumSet outer) { switch (doc) { @@ -98,7 +94,7 @@ protected void renderDoc(@NotNull Cursor cursor, @NotNull Doc doc, EnumSet renderHyperLinked(cursor, text, outer); case Doc.Image image -> renderImage(cursor, image, outer); case Doc.Styled styled -> renderStyled(cursor, styled, outer); - case Doc.Line d -> renderHardLineBreak(cursor, outer); + case Doc.Line _ -> renderHardLineBreak(cursor, outer); case Doc.FlatAlt alt -> renderFlatAlt(cursor, alt, outer); case Doc.Cat cat -> cat.inner().forEach(inner -> renderDoc(cursor, inner, outer)); case Doc.Nest nest -> renderNest(cursor, nest, outer); @@ -112,26 +108,25 @@ protected void renderDoc(@NotNull Cursor cursor, @NotNull Doc doc, EnumSet renderInlineMath(cursor, inlineMath, outer); case Doc.MathBlock mathBlock -> renderMathBlock(cursor, mathBlock, outer); case Doc.Tooltip tooltip -> renderTooltip(cursor, tooltip, outer); - case Doc.Empty _ -> {} + case Doc.Empty _ -> { } } } private static final @NotNull Map unicodeMapping = Map.ofEntries( - Tuple.of("Sig", "\u03A3"), - Tuple.of("/\\", "\u2227"), - Tuple.of("\\/", "\u2228"), - Tuple.of("=>", "\u21D2"), - Tuple.of("ulift", "\u2191"), - Tuple.of("forall", "\u2200"), - Tuple.of("->", "\u2192"), - Tuple.of("_|_", "\u22A5"), - Tuple.of("top", "\u22A4"), - Tuple.of("(|", "\u2987"), - Tuple.of("|)", "\u2988"), - Tuple.of("{|", "\u2983"), - Tuple.of("|}", "\u2984"), - Tuple.of("[|", "\u27E6"), - Tuple.of("|]", "\u27E7") + Tuple.of("/\\", "∧"), + Tuple.of("\\/", "∨"), + Tuple.of("=>", "⇒"), + Tuple.of("ulift", "↑"), + Tuple.of("forall", "∀"), + Tuple.of("->", "→"), + Tuple.of("_|_", "⊥"), + Tuple.of("top", "⊤"), + Tuple.of("(|", "⦇"), + Tuple.of("|)", "⦈"), + Tuple.of("{|", "⦃"), + Tuple.of("|}", "⦄"), + Tuple.of("[|", "⟦"), + Tuple.of("|]", "⟧") ); protected void renderSpecialSymbol(@NotNull Cursor cursor, @NotNull String text, EnumSet outer) { @@ -169,17 +164,13 @@ protected void renderStyled(@NotNull Cursor cursor, @NotNull Doc.Styled styled, stylist.format(styled.styles(), cursor, outer, () -> renderDoc(cursor, styled.doc(), outer)); } - protected @NotNull StringStylist prepareStylist() { - return config.getStylist(); - } + protected @NotNull StringStylist prepareStylist() { return config.getStylist(); } protected void renderPlainText(@NotNull Cursor cursor, @NotNull String content, EnumSet outer) { cursor.visibleContent(escapePlainText(content, outer)); } - protected @NotNull String escapePlainText(@NotNull String content, EnumSet outer) { - return content; - } + protected @NotNull String escapePlainText(@NotNull String content, EnumSet outer) { return content; } /** * This line break makes target source code beautiful (like .tex or .md generated from Doc). @@ -191,7 +182,7 @@ protected void renderPlainText(@NotNull Cursor cursor, @NotNull String content, * @apiNote This is called by {@link #renderCodeBlock}, {@link #renderMathBlock}, {@link #formatList}, * and other block rendering methods to separate the current block from the previous one. */ - protected void renderBlockSeparator(@NotNull Cursor cursor, EnumSet outer) { + protected void renderBlockSeparator(@NotNull Cursor cursor, EnumSet ignoredOuter) { cursor.lineBreakWith("\n"); } diff --git a/pretty/src/main/java/org/aya/pretty/backend/string/StringStylist.java b/pretty/src/main/java/org/aya/pretty/backend/string/StringStylist.java index 65873fe079..ed16b4f834 100644 --- a/pretty/src/main/java/org/aya/pretty/backend/string/StringStylist.java +++ b/pretty/src/main/java/org/aya/pretty/backend/string/StringStylist.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; @@ -16,5 +16,10 @@ public StringStylist(@NotNull ColorScheme colorScheme, @NotNull StyleFamily styl super(colorScheme, styleFamily); } - public abstract void format(@NotNull Seq