Skip to content

Commit

Permalink
show cursor much more often during progress bar printing to ensure it…
Browse files Browse the repository at this point in the history
… is not lost every time a process is killed
  • Loading branch information
jurgenvinju committed Jun 20, 2024
1 parent 28238b9 commit f656c0a
Showing 1 changed file with 15 additions and 9 deletions.
24 changes: 15 additions & 9 deletions src/org/rascalmpl/repl/TerminalProgressBarMonitor.java
Original file line number Diff line number Diff line change
Expand Up @@ -477,16 +477,12 @@ static String showCursor() {
* Simply print the bars. No cursor movement here. Hiding the cursor prevents flickering.
*/
private void printBars() {
if (bars.isEmpty()) {
// no more bars to show, so cursor goes back.
writer.write(ANSI.showCursor());
}

for (var pb : bars) {
pb.write();
}

writer.flush();

}

/**
Expand Down Expand Up @@ -516,8 +512,6 @@ public synchronized void jobStart(String name, int workShare, int totalWork) {
if (bars.size() == 0) {
// first new job, we take time to react to window resizing
lineWidth = tm.getWidth();
// remove the cursor
writer.write(ANSI.hideCursor());
}

if (totalWork == 0) {
Expand All @@ -528,33 +522,43 @@ public synchronized void jobStart(String name, int workShare, int totalWork) {

var pb = findBarByName(name);

if (pb == null) {
writer.write(ANSI.hideCursor());

if (pb == null) {
eraseBars(); // to make room for the new bars
bars.add(new ProgressBar(name, totalWork));
printBars(); // probably one line longer than before!
printBars(); // probably one line longer than before!
}
else {
// Zeno-bar: we add the new work to the already existing work
pb.max += totalWork;
pb.nesting++;
pb.update();
}

writer.write(ANSI.showCursor());
writer.flush();
}

@Override
public synchronized void jobStep(String name, String message, int workShare) {
ProgressBar pb = findBarByName(name);

if (pb != null) {
writer.write(ANSI.hideCursor());
pb.worked(workShare, message);
pb.update();
writer.write(ANSI.showCursor());
writer.flush();
}
}

@Override
public synchronized int jobEnd(String name, boolean succeeded) {
var pb = findBarByName(name);

writer.write(ANSI.hideCursor());

if (pb != null && --pb.nesting == -1) {
eraseBars();
// write it one last time into the scrollback buffer (on top)
Expand All @@ -570,6 +574,8 @@ else if (pb != null) {
pb.update();
}

writer.write(ANSI.showCursor());

return -1;
}

Expand Down

0 comments on commit f656c0a

Please sign in to comment.