Merge branch 'main' into syntax-role-modifiers

usethesource · Nov 29, 2023 · 4cd9e61 · 4cd9e61
2 parents 5ed339c + e17f90a
commit 4cd9e61
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 18 deletions.
diff --git a/src/org/rascalmpl/library/Prelude.java b/src/org/rascalmpl/library/Prelude.java
@@ -923,15 +923,15 @@ public void iprint(IValue arg, IInteger lineLimit){
 	        // ignore, it's what we wanted
 	    }
 		catch (IOException e) {
-			RuntimeExceptionFactory.io(values.string("Could not print indented value"));
+			throw RuntimeExceptionFactory.io(values.string("Could not print indented value"));
 		}
 		finally {
-		    try {
-		        output.flush();
-		        output.close();
-		    }
-		    catch (IOException e) {
-		    }
+			try {
+				output.flush();
+			}
+			catch (IOException e) {
+				// ignore
+			}
 		}
 	}
 

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 {