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
usethesource · Nov 29, 2023 · e17f90a · e17f90a
1 parent 7687359
commit e17f90a
Showing 1 changed file with 13 additions and 11 deletions.
diff --git 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 {