1.1 --- a/src/Pure/General/exn.scala	Thu Aug 11 20:32:44 2011 +0200
     1.2 +++ b/src/Pure/General/exn.scala	Fri Aug 12 11:41:26 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  object Exn
     1.6  {
     1.7 -  /* runtime exceptions as values */
     1.8 +  /* exceptions as values */
     1.9  
    1.10    sealed abstract class Result[A]
    1.11    case class Res[A](res: A) extends Result[A]
    1.12 @@ -24,5 +24,17 @@
    1.13        case Res(x) => x
    1.14        case Exn(exn) => throw exn
    1.15      }
    1.16 +
    1.17 +
    1.18 +  /* message */
    1.19 +
    1.20 +  private val runtime_exception = Class.forName("java.lang.RuntimeException")
    1.21 +
    1.22 +  def message(exn: Throwable): String =
    1.23 +    if (exn.getClass == runtime_exception) {
    1.24 +      val msg = exn.getMessage
    1.25 +      if (msg == null) "Error" else msg
    1.26 +    }
    1.27 +    else exn.toString
    1.28  }
    1.29