# HG changeset patch
# User wenzelm
# Date 1697115599 -7200
# Node ID 5578341489cbddd988b839349009bea336649ecb
# Parent  f971ccccfd8ed5f2766e09af83978a31bc5ad1c0
further clarification of Exn.is_interrupt_proper vs. overall Exn.is_interrupt;

diff -r f971ccccfd8e -r 5578341489cb src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Oct 12 15:45:06 2023 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Oct 12 14:59:59 2023 +0200
@@ -236,7 +236,7 @@
         val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
         val test = Isabelle_Thread.expose_interrupt_result ();
         val _ =
-          if ok andalso not (Exn.is_interrupt_exn test) then ()
+          if ok andalso not (Exn.is_interrupt_proper_exn test) then ()
           else if null (cancel_now group) then ()
           else cancel_later group;
         val _ = broadcast work_finished;
@@ -361,7 +361,7 @@
     Exn.Res res => res
   | Exn.Exn exn =>
      (Multithreading.tracing 1 (fn () => "SCHEDULER: " ^ General.exnMessage exn);
-      if Exn.is_interrupt exn then
+      if Exn.is_interrupt_proper exn then
        (List.app cancel_later (cancel_all ());
         signal work_available; true)
       else
@@ -425,7 +425,7 @@
       (case Exn.capture_body (fn () => Single_Assignment.assign result res) of
         Exn.Exn (exn as Fail _) =>
           (case Single_Assignment.peek result of
-            SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt e then e else exn)
+            SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt_proper e then e else exn)
           | _ => Exn.reraise exn)
       | _ => ());
     val ok =
@@ -499,7 +499,7 @@
   (case peek x of
     NONE => Exn.Exn (Fail "Unfinished future")
   | SOME result =>
-      if Exn.is_interrupt_exn result then
+      if Exn.is_interrupt_proper_exn result then
         (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of
           [] => result
         | exns => Exn.Exn (Par_Exn.make exns))
@@ -562,7 +562,9 @@
     in
       (case Exn.capture_body (fn () => run join_results futures) of
         Exn.Res res => res
-      | Exn.Exn exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn))
+      | Exn.Exn exn =>
+         (if Exn.is_interrupt_proper exn then cancel_group group else ();
+          Exn.reraise exn))
     end);
 
 
@@ -651,7 +653,7 @@
         Exn.Res res => res
       | Exn.Exn (Fail _) => true
       | Exn.Exn exn =>
-          if Exn.is_interrupt exn
+          if Exn.is_interrupt_proper exn
           then raise Fail "Concurrent attempt to fulfill promise"
           else Exn.reraise exn);
     fun job () =
diff -r f971ccccfd8e -r 5578341489cb src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Thu Oct 12 15:45:06 2023 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Thu Oct 12 14:59:59 2023 +0200
@@ -61,7 +61,7 @@
       | Result res => not (Future.is_finished res));
 
 fun is_finished_future res =
-  Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res));
+  Future.is_finished res andalso not (Exn.is_interrupt_proper_exn (Future.join_result res));
 
 fun is_finished (Value _) = true
   | is_finished (Lazy var) =
@@ -105,7 +105,7 @@
                     val _ = Exn.capture_body (fn () => Future.fulfill_result x res0);
                     val res = Future.get_result x;
                     val _ =
-                      if not (Exn.is_interrupt_exn res) then
+                      if not (Exn.is_interrupt_proper_exn res) then
                         Synchronized.assign var (Result (Future.value_result res))
                       else if strict then
                         Synchronized.assign var
diff -r f971ccccfd8e -r 5578341489cb src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Thu Oct 12 15:45:06 2023 +0200
+++ b/src/Pure/Concurrent/timeout.ML	Thu Oct 12 14:59:59 2023 +0200
@@ -47,8 +47,11 @@
         val stop = Time.now ();
         val was_timeout = not (Event_Timer.cancel request);
         val test = Isabelle_Thread.expose_interrupt_result ();
+        val was_interrupt =
+          Exn.is_interrupt_proper_exn result orelse
+          Exn.is_interrupt_proper_exn test;
       in
-        if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
+        if was_timeout andalso was_interrupt
         then raise TIMEOUT (stop - start)
         else (Exn.release test; Exn.release result)
       end);