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

     2.1 --- a/src/Pure/General/exn.scala	Thu Aug 11 20:32:44 2011 +0200
     2.2 +++ b/src/Pure/General/exn.scala	Fri Aug 12 11:41:26 2011 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  
     2.5  object Exn
     2.6  {
     2.7 -  /* runtime exceptions as values */
     2.8 +  /* exceptions as values */
     2.9  
    2.10    sealed abstract class Result[A]
    2.11    case class Res[A](res: A) extends Result[A]
    2.12 @@ -24,5 +24,17 @@
    2.13        case Res(x) => x
    2.14        case Exn(exn) => throw exn
    2.15      }
    2.16 +
    2.17 +
    2.18 +  /* message */
    2.19 +
    2.20 +  private val runtime_exception = Class.forName("java.lang.RuntimeException")
    2.21 +
    2.22 +  def message(exn: Throwable): String =
    2.23 +    if (exn.getClass == runtime_exception) {
    2.24 +      val msg = exn.getMessage
    2.25 +      if (msg == null) "Error" else msg
    2.26 +    }
    2.27 +    else exn.toString
    2.28  }
    2.29  

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

     4.1 --- a/src/Pure/System/invoke_scala.scala	Thu Aug 11 20:32:44 2011 +0200
     4.2 +++ b/src/Pure/System/invoke_scala.scala	Fri Aug 12 11:41:26 2011 +0200
     4.3 @@ -57,10 +57,8 @@
     4.4          Exn.capture { f(arg) } match {
     4.5            case Exn.Res(null) => (Tag.NULL, "")
     4.6            case Exn.Res(res) => (Tag.OK, res)
     4.7 -          case Exn.Exn(ERROR(msg)) => (Tag.ERROR, msg)
     4.8 -          case Exn.Exn(e) => (Tag.ERROR, e.toString)
     4.9 +          case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
    4.10          }
    4.11 -      case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
    4.12 -      case Exn.Exn(e) => (Tag.FAIL, e.toString)
    4.13 +      case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
    4.14      }
    4.15  }

     5.1 --- a/src/Pure/library.scala	Thu Aug 11 20:32:44 2011 +0200
     5.2 +++ b/src/Pure/library.scala	Fri Aug 12 11:41:26 2011 +0200
     5.3 @@ -20,19 +20,12 @@
     5.4  {
     5.5    /* user errors */
     5.6  
     5.7 -  private val runtime_exception = Class.forName("java.lang.RuntimeException")
     5.8 -
     5.9    object ERROR
    5.10    {
    5.11      def apply(message: String): Throwable = new RuntimeException(message)
    5.12      def unapply(exn: Throwable): Option[String] =
    5.13        exn match {
    5.14 -        case e: RuntimeException =>
    5.15 -          if (e.getClass != runtime_exception) Some(e.toString)
    5.16 -          else {
    5.17 -            val msg = e.getMessage
    5.18 -            Some(if (msg == null) "Error" else msg)
    5.19 -          }
    5.20 +        case e: RuntimeException => Some(Exn.message(e))
    5.21          case _ => None
    5.22        }
    5.23    }