# HG changeset patch
# User wenzelm
# Date 1343143999 -7200
# Node ID 819f7a5f3e7fab39bd3221ca1c7e2cbd07d93915
# Parent  146090de047474ea903ffb585ba9672a1ade0541
more general notion of user ERROR (cf. 44f56fe01528);

diff -r 146090de0474 -r 819f7a5f3e7f src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Tue Jul 24 17:20:54 2012 +0200
+++ b/src/Pure/General/exn.scala	Tue Jul 24 17:33:19 2012 +0200
@@ -31,16 +31,19 @@
 
   private val runtime_exception = Class.forName("java.lang.RuntimeException")
 
-  def message(exn: Throwable): String =
+  def user_message(exn: Throwable): Option[String] =
     if (exn.isInstanceOf[java.io.IOException]) {
       val msg = exn.getMessage
-      if (msg == null) "I/O error"
-      else "I/O error: " + msg
+      Some(if (msg == null) "I/O error" else "I/O error: " + msg)
     }
     else if (exn.getClass == runtime_exception) {
       val msg = exn.getMessage
-      if (msg == null) "Error" else msg
+      Some(if (msg == null) "Error" else msg)
     }
-    else exn.toString
+    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
+    else None
+
+  def message(exn: Throwable): String =
+    user_message(exn) getOrElse exn.toString
 }
 
diff -r 146090de0474 -r 819f7a5f3e7f src/Pure/library.scala
--- a/src/Pure/library.scala	Tue Jul 24 17:20:54 2012 +0200
+++ b/src/Pure/library.scala	Tue Jul 24 17:33:19 2012 +0200
@@ -24,11 +24,7 @@
   object ERROR
   {
     def apply(message: String): Throwable = new RuntimeException(message)
-    def unapply(exn: Throwable): Option[String] =
-      exn match {
-        case e: RuntimeException => Some(Exn.message(e))
-        case _ => None
-      }
+    def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
   }
 
   def error(message: String): Nothing = throw ERROR(message)