# HG changeset patch
# User wenzelm
# Date 1343133368 -7200
# Node ID 44f56fe015286142db753c2fe80106bd9aae0464
# Parent  02dd825f5a4eaf5f41bd06fef36b9a8e59144b6b
human-readable I/O error;

diff -r 02dd825f5a4e -r 44f56fe01528 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Tue Jul 24 14:07:44 2012 +0200
+++ b/src/Pure/General/exn.scala	Tue Jul 24 14:36:08 2012 +0200
@@ -32,7 +32,12 @@
   private val runtime_exception = Class.forName("java.lang.RuntimeException")
 
   def message(exn: Throwable): String =
-    if (exn.getClass == runtime_exception) {
+    if (exn.isInstanceOf[java.io.IOException]) {
+      val msg = exn.getMessage
+      if (msg == null) "I/O error"
+      else "I/O error: " + msg
+    }
+    else if (exn.getClass == runtime_exception) {
       val msg = exn.getMessage
       if (msg == null) "Error" else msg
     }