src/Pure/General/exn.scala

--- a/src/Pure/General/exn.scala	Tue Jul 24 17:20:54 2012 +0200
+++ b/src/Pure/General/exn.scala	Tue Jul 24 17:33:19 2012 +0200
@@ -31,16 +31,19 @@
 
   private val runtime_exception = Class.forName("java.lang.RuntimeException")
 
-  def message(exn: Throwable): String =
+  def user_message(exn: Throwable): Option[String] =
     if (exn.isInstanceOf[java.io.IOException]) {
       val msg = exn.getMessage
-      if (msg == null) "I/O error"
-      else "I/O error: " + msg
+      Some(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
+      Some(if (msg == null) "Error" else msg)
     }
-    else exn.toString
+    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
+    else None
+
+  def message(exn: Throwable): String =
+    user_message(exn) getOrElse exn.toString
 }