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