--- a/src/Pure/General/exn.scala Thu Nov 12 11:46:53 2020 +0100
+++ b/src/Pure/General/exn.scala Thu Nov 12 12:10:17 2020 +0100
@@ -93,6 +93,12 @@
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)
--- a/src/Pure/Tools/build.scala Thu Nov 12 11:46:53 2020 +0100
+++ b/src/Pure/Tools/build.scala Thu Nov 12 12:10:17 2020 +0100
@@ -386,7 +386,7 @@
Present.finish(store.browser_info, graph_pdf, info, session_name)
Nil
}
- catch { case ERROR(msg) => List(msg) case e@Exn.Interrupt() => List(Exn.message(e)) }
+ catch { case Exn.Interrupt.ERROR(msg) => List(msg) }
val result =
{