1.1 --- a/src/Pure/General/exn.scala	Tue Jul 24 14:07:44 2012 +0200
     1.2 +++ b/src/Pure/General/exn.scala	Tue Jul 24 14:36:08 2012 +0200
     1.3 @@ -32,7 +32,12 @@
     1.4    private val runtime_exception = Class.forName("java.lang.RuntimeException")
     1.5  
     1.6    def message(exn: Throwable): String =
     1.7 -    if (exn.getClass == runtime_exception) {
     1.8 +    if (exn.isInstanceOf[java.io.IOException]) {
     1.9 +      val msg = exn.getMessage
    1.10 +      if (msg == null) "I/O error"
    1.11 +      else "I/O error: " + msg
    1.12 +    }
    1.13 +    else if (exn.getClass == runtime_exception) {
    1.14        val msg = exn.getMessage
    1.15        if (msg == null) "Error" else msg
    1.16      }