From f26a445fd79af0a775c19baf4646ea46f5ea4f2e Mon Sep 17 00:00:00 2001 From: "Jurgen J. Vinju" Date: Wed, 3 Apr 2024 17:26:52 +0200 Subject: [PATCH] this fixes off-by-one issues that are only visible if there is extra room atthe bottom of the terminal --- .../repl/TerminalProgressBarMonitor.java | 48 +++++++++++++++++-- 1 file changed, 45 insertions(+), 3 deletions(-) diff --git a/src/org/rascalmpl/repl/TerminalProgressBarMonitor.java b/src/org/rascalmpl/repl/TerminalProgressBarMonitor.java index 6c3aeba2475..f88d4703984 100644 --- a/src/org/rascalmpl/repl/TerminalProgressBarMonitor.java +++ b/src/org/rascalmpl/repl/TerminalProgressBarMonitor.java @@ -1,6 +1,7 @@ package org.rascalmpl.repl; import java.io.FilterOutputStream; +import java.io.FilterWriter; import java.io.IOException; import java.io.OutputStream; import java.io.PrintWriter; @@ -49,13 +50,53 @@ public class TerminalProgressBarMonitor extends FilterOutputStream implements IR */ private final String encoding; + /** + * Will make everything slow, but easier to spot mistakes + */ + private final boolean debug = false; + + @SuppressWarnings("resource") public TerminalProgressBarMonitor(OutputStream out, Terminal tm) { super(out); this.encoding = tm.getOutputEncoding() != null ? tm.getOutputEncoding() : "UTF8"; - this.writer = new PrintWriter(out, true, Charset.forName(encoding)); + PrintWriter theWriter = new PrintWriter(out, true, Charset.forName(encoding)); + this.writer = debug ? new PrintWriter(new AlwaysFlushAlwaysShowCursor(theWriter)) : theWriter; this.lineWidth = tm.getWidth(); } + /** + * Use this for debugging terminal cursor movements, step by step. + */ + private static class AlwaysFlushAlwaysShowCursor extends FilterWriter { + + public AlwaysFlushAlwaysShowCursor(PrintWriter out) { + super(out); + } + + @Override + public void write(int c) throws IOException { + out.write(c); + out.write(ANSI.showCursor()); + out.flush(); + } + + @Override + public void write(char[] cbuf, int off, int len) throws IOException { + out.write(cbuf, off, len); + out.write(ANSI.showCursor()); + out.flush(); + } + + @Override + public void write(String str, int off, int len) throws IOException { + out.write(str, off, len); + out.write(ANSI.showCursor()); + out.flush(); + } + + + } + /** * Represents one currently running progress bar */ @@ -102,7 +143,7 @@ void update() { writer.write(ANSI.hideCursor()); writer.write(ANSI.moveUp(bars.size() - bars.indexOf(this))); write(); - writer.write(ANSI.moveDown(bars.size() - bars.indexOf(this))); + writer.write(ANSI.moveDown(bars.size() - bars.indexOf(this) - 1 /* already wrote a \n */)); writer.write(ANSI.showCursor()); writer.flush(); } @@ -203,7 +244,8 @@ public void done() { */ private void eraseBars() { if (bars.isEmpty()) { - writer.println(); + // writer.println(); + return; } writer.write(ANSI.hideCursor());