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