# HG changeset patch
# User wenzelm
# Date 1310418927 -7200
# Node ID ab11dcfa3e6d3e4829425c39310a46b617616a9c
# Parent  50ce6f602931f19dccecafd5fa9f88209b553459
tuned error messages;

diff -r 50ce6f602931 -r ab11dcfa3e6d src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Jul 11 23:15:04 2011 +0200
+++ b/src/Pure/library.scala	Mon Jul 11 23:15:27 2011 +0200
@@ -20,14 +20,19 @@
 {
   /* user errors */
 
+  private val runtime_exception = Class.forName("java.lang.RuntimeException")
+
   object ERROR
   {
     def apply(message: String): Throwable = new RuntimeException(message)
     def unapply(exn: Throwable): Option[String] =
       exn match {
         case e: RuntimeException =>
-          val msg = e.getMessage
-          Some(if (msg == null) "Error" else msg)
+          if (e.getClass != runtime_exception) Some(e.toString)
+          else {
+            val msg = e.getMessage
+            Some(if (msg == null) "Error" else msg)
+          }
         case _ => None
       }
   }