human-readable I/O error;

--- 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
     }