clarified Exn.message;

--- a/src/Pure/General/exn.ML	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/Pure/General/exn.ML	Fri Aug 12 11:41:26 2011 +0200
@@ -30,7 +30,7 @@
 structure Exn: EXN =
 struct
 
-(* runtime exceptions as values *)
+(* exceptions as values *)
 
 datatype 'a result =
   Res of 'a |

--- a/src/Pure/General/exn.scala	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/Pure/General/exn.scala	Fri Aug 12 11:41:26 2011 +0200
@@ -9,7 +9,7 @@
 
 object Exn
 {
-  /* runtime exceptions as values */
+  /* exceptions as values */
 
   sealed abstract class Result[A]
   case class Res[A](res: A) extends Result[A]
@@ -24,5 +24,17 @@
       case Res(x) => x
       case Exn(exn) => throw exn
     }
+
+
+  /* message */
+
+  private val runtime_exception = Class.forName("java.lang.RuntimeException")
+
+  def message(exn: Throwable): String =
+    if (exn.getClass == runtime_exception) {
+      val msg = exn.getMessage
+      if (msg == null) "Error" else msg
+    }
+    else exn.toString
 }
 

--- a/src/Pure/PIDE/isar_document.scala	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Fri Aug 12 11:41:26 2011 +0200
@@ -153,7 +153,7 @@
                   Document.Node.Header(_, Exn.Res(Thy_Header.Header(a, b, c)))) =>
                 (Nil, triple(string, list(string), list(string))(a, b, c)) },
             { case Document.Node.Update_Header(
-                  Document.Node.Header(_, Exn.Exn(ERROR(a)))) => (List(a), Nil) }))))
+                  Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
       YXML.string_of_body(encode(edits)) }
 
     input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)

--- a/src/Pure/System/invoke_scala.scala	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/Pure/System/invoke_scala.scala	Fri Aug 12 11:41:26 2011 +0200
@@ -57,10 +57,8 @@
         Exn.capture { f(arg) } match {
           case Exn.Res(null) => (Tag.NULL, "")
           case Exn.Res(res) => (Tag.OK, res)
-          case Exn.Exn(ERROR(msg)) => (Tag.ERROR, msg)
-          case Exn.Exn(e) => (Tag.ERROR, e.toString)
+          case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
         }
-      case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
-      case Exn.Exn(e) => (Tag.FAIL, e.toString)
+      case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
     }
 }

--- a/src/Pure/library.scala	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/Pure/library.scala	Fri Aug 12 11:41:26 2011 +0200
@@ -20,19 +20,12 @@
 {
   /* 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 =>
-          if (e.getClass != runtime_exception) Some(e.toString)
-          else {
-            val msg = e.getMessage
-            Some(if (msg == null) "Error" else msg)
-          }
+        case e: RuntimeException => Some(Exn.message(e))
         case _ => None
       }
   }