1.1 --- a/src/Pure/library.scala	Mon Jul 11 23:15:04 2011 +0200
     1.2 +++ b/src/Pure/library.scala	Mon Jul 11 23:15:27 2011 +0200
     1.3 @@ -20,14 +20,19 @@
     1.4  {
     1.5    /* user errors */
     1.6  
     1.7 +  private val runtime_exception = Class.forName("java.lang.RuntimeException")
     1.8 +
     1.9    object ERROR
    1.10    {
    1.11      def apply(message: String): Throwable = new RuntimeException(message)
    1.12      def unapply(exn: Throwable): Option[String] =
    1.13        exn match {
    1.14          case e: RuntimeException =>
    1.15 -          val msg = e.getMessage
    1.16 -          Some(if (msg == null) "Error" else msg)
    1.17 +          if (e.getClass != runtime_exception) Some(e.toString)
    1.18 +          else {
    1.19 +            val msg = e.getMessage
    1.20 +            Some(if (msg == null) "Error" else msg)
    1.21 +          }
    1.22          case _ => None
    1.23        }
    1.24    }