# HG changeset patch
# User wenzelm
# Date 1695391878 -7200
# Node ID cde40295ffd6a0b12f9e3911fca121e543b0509b
# Parent  46891e209d72a6094d176d75b71213eb75fcf10f
clarified signature;
update component;

diff -r 46891e209d72 -r cde40295ffd6 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri Sep 22 00:05:11 2023 +0200
+++ b/Admin/components/components.sha1	Fri Sep 22 16:11:18 2023 +0200
@@ -169,6 +169,7 @@
 7b1ce9bd85e33076fa7022eeb66ce15915d078d9 isabelle_setup-20221020.tar.gz
 cb9f061ccd7c6f90d00c8aa115aeea8679f3f996 isabelle_setup-20221028.tar.gz
 f582c621471583d06e00007c6acc01376c7395af isabelle_setup-20230206.tar.gz
+d30109fe63cec35c31cee9ffd17ae3a13c1e6a33 isabelle_setup-20230922.tar.gz
 0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
 e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
 3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
diff -r 46891e209d72 -r cde40295ffd6 Admin/components/main
--- a/Admin/components/main	Fri Sep 22 00:05:11 2023 +0200
+++ b/Admin/components/main	Fri Sep 22 16:11:18 2023 +0200
@@ -11,7 +11,7 @@
 foiltex-2.1.4b
 idea-icons-20210508
 isabelle_fonts-20211004
-isabelle_setup-20230206
+isabelle_setup-20230922
 jdk-17.0.7
 jedit-20211103
 jfreechart-1.5.3
diff -r 46891e209d72 -r cde40295ffd6 src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Fri Sep 22 00:05:11 2023 +0200
+++ b/src/Pure/General/exn.ML	Fri Sep 22 16:11:18 2023 +0200
@@ -26,6 +26,7 @@
   val map_res: ('a -> 'b) -> 'a result -> 'b result
   val maps_res: ('a -> 'b result) -> 'a result -> 'b result
   val map_exn: (exn -> exn) -> 'a result -> 'a result
+  val cause: exn -> exn
   val is_interrupt: exn -> bool
   val is_interrupt_exn: 'a result -> bool
   val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
@@ -89,9 +90,13 @@
 
 (* interrupts *)
 
-fun is_interrupt Thread.Thread.Interrupt = true
-  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
-  | is_interrupt _ = false;
+fun cause (IO.Io {cause = exn, ...}) = cause exn
+  | cause exn = exn;
+
+fun is_interrupt exn =
+  (case cause exn of
+    Thread.Thread.Interrupt => true
+  | _ => false);
 
 fun is_interrupt_exn (Exn exn) = is_interrupt exn
   | is_interrupt_exn _ = false;
diff -r 46891e209d72 -r cde40295ffd6 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Fri Sep 22 00:05:11 2023 +0200
+++ b/src/Pure/General/exn.scala	Fri Sep 22 16:11:18 2023 +0200
@@ -78,6 +78,9 @@
 
   /* interrupts */
 
+  def cause(exn: Throwable): Throwable =
+    isabelle.setup.Exn.cause(exn)
+
   def is_interrupt(exn: Throwable): Boolean =
     isabelle.setup.Exn.is_interrupt(exn)
 
diff -r 46891e209d72 -r cde40295ffd6 src/Tools/Setup/src/Exn.java
--- a/src/Tools/Setup/src/Exn.java	Fri Sep 22 00:05:11 2023 +0200
+++ b/src/Tools/Setup/src/Exn.java	Fri Sep 22 16:11:18 2023 +0200
@@ -16,15 +16,18 @@
 {
     /* interrupts */
 
+    public static Throwable cause(Throwable exn)
+    {
+        Throwable e = exn;
+        while (e != null && e.getCause() != null) {
+            e = e.getCause();
+        }
+        return e;
+    }
+
     public static boolean is_interrupt(Throwable exn)
     {
-        boolean found_interrupt = false;
-        Throwable e = exn;
-        while (!found_interrupt && e != null) {
-            found_interrupt = e instanceof InterruptedException;
-            e = e.getCause();
-        }
-        return found_interrupt;
+        return cause(exn) instanceof InterruptedException;
     }
 
     public static int failure_rc(Throwable exn)