--- 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
--- 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
--- 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;
--- 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)
--- 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)