tuned error messages;

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