more explicit exception User_Error, with value-oriented equality;

--- a/src/Pure/General/exn.scala	Sat Mar 14 20:08:03 2015 +0100
+++ b/src/Pure/General/exn.scala	Sat Mar 14 20:49:10 2015 +0100
@@ -79,17 +79,18 @@
 
   /* message */
 
-  private val runtime_exception = Class.forName("java.lang.RuntimeException")
-
   def user_message(exn: Throwable): Option[String] =
-    if (exn.isInstanceOf[java.io.IOException]) {
-      val msg = exn.getMessage
-      Some(if (msg == null) "I/O error" else "I/O error: " + msg)
-    }
-    else if (exn.getClass == runtime_exception) {
+    if (exn.getClass == classOf[RuntimeException] ||
+        exn.getClass == classOf[Library.User_Error])
+    {
       val msg = exn.getMessage
       Some(if (msg == null || msg == "") "Error" else msg)
     }
+    else if (exn.isInstanceOf[java.io.IOException])
+    {
+      val msg = exn.getMessage
+      Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
+    }
     else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
     else None
 

--- a/src/Pure/library.scala	Sat Mar 14 20:08:03 2015 +0100
+++ b/src/Pure/library.scala	Sat Mar 14 20:49:10 2015 +0100
@@ -16,9 +16,21 @@
 {
   /* user errors */
 
+  class User_Error(message: String) extends RuntimeException(message)
+  {
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: User_Error => message == other.getMessage
+        case _ => false
+      }
+    override def hashCode: Int = message.hashCode
+
+    override def toString: String = "ERROR(" + message + ")"
+  }
+
   object ERROR
   {
-    def apply(message: String): Throwable = new RuntimeException(message)
+    def apply(message: String): User_Error = new User_Error(message)
     def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
   }