From e17f90a9644171667ed9c447da578373e8b48558 Mon Sep 17 00:00:00 2001 From: "Jurgen J. Vinju" Date: Wed, 29 Nov 2023 17:52:58 +0100 Subject: [PATCH] fixed issue that terminal error can not be printed sometimes because the error stream is closed by the handler before it is printed; as detected in #1895 --- src/org/rascalmpl/repl/BaseREPL.java | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/src/org/rascalmpl/repl/BaseREPL.java b/src/org/rascalmpl/repl/BaseREPL.java index 74217675357..4540685a344 100755 --- a/src/org/rascalmpl/repl/BaseREPL.java +++ b/src/org/rascalmpl/repl/BaseREPL.java @@ -363,19 +363,21 @@ public void run() throws IOException { // we are closing down, so do nothing, the finally clause will take care of it } catch (Throwable e) { - try (PrintWriter err = new PrintWriter(errorWriter, true)) { + PrintWriter err = new PrintWriter(errorWriter, true); + + if (!err.checkError()) { err.println("Unexpected (uncaught) exception, closing the REPL: "); - if (!err.checkError()) { - err.print(e.toString()); - e.printStackTrace(err); - } - else { - System.err.print(e.toString()); - e.printStackTrace(); - } - err.flush(); + err.print(e.toString()); + e.printStackTrace(err); } - errorWriter.flush(); + else { + System.err.println("Unexpected (uncaught) exception, closing the REPL: "); + System.err.print(e.toString()); + e.printStackTrace(System.err); + } + + err.flush(); + throw e; } finally {