tuned signature;
authorwenzelm
Thu, 12 Nov 2020 12:10:17 +0100
changeset 72832 b2bbe2e6575d
parent 72831 c806eeb9138c
child 72833 e8d7dc1c229c
tuned signature;
src/Pure/General/exn.scala
src/Pure/Tools/build.scala
--- 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 =
         {