src/Pure/General/exn.scala

     try { Res(e) }
     catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) }
 
   object Interrupt
   {
+    object ERROR
+    {
+      def unapply(exn: Throwable): Option[String] =
+        if (is_interrupt(exn)) Some(message(exn)) else user_message(exn)
+    }
+
     def apply(): Throwable = new InterruptedException("Interrupt")
     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
 
     def dispose() { Thread.interrupted }
     def expose() { if (Thread.interrupted) throw apply() }