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 }