# HG changeset patch # User wenzelm # Date 1695671938 -7200 # Node ID eb2255d241da2091b5d3aab024469ad89326fc02 # Parent a44ac17ae227100ac544083d62033901ef988d3a clarified signature; diff -r a44ac17ae227 -r eb2255d241da src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Mon Sep 25 21:46:38 2023 +0200 +++ b/src/Pure/Concurrent/future.ML Mon Sep 25 21:58:58 2023 +0200 @@ -234,7 +234,7 @@ val _ = SYNCHRONIZED "finish" (fn () => let val maximal = Unsynchronized.change_result queue (Task_Queue.finish task); - val test = Exn.capture Isabelle_Thread.expose_interrupt (); + val test = Isabelle_Thread.expose_interrupt_result (); val _ = if ok andalso not (Exn.is_interrupt_exn test) then () else if null (cancel_now group) then () diff -r a44ac17ae227 -r eb2255d241da src/Pure/Concurrent/isabelle_thread.ML --- a/src/Pure/Concurrent/isabelle_thread.ML Mon Sep 25 21:46:38 2023 +0200 +++ b/src/Pure/Concurrent/isabelle_thread.ML Mon Sep 25 21:58:58 2023 +0200 @@ -25,6 +25,7 @@ val interrupt_exn: 'a Exn.result val interrupt_self: unit -> 'a val interrupt_other: T -> unit + val expose_interrupt_result: unit -> unit Exn.result val expose_interrupt: unit -> unit (*exception Interrupt*) val try_catch: (unit -> 'a) -> (exn -> 'a) -> 'a val try_finally: (unit -> 'a) -> (unit -> unit) -> 'a @@ -122,13 +123,15 @@ fun interrupt_other t = Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => (); -fun expose_interrupt () = +fun expose_interrupt_result () = let val orig_atts = Thread_Attributes.safe_interrupts (Thread_Attributes.get_attributes ()); val _ = Thread_Attributes.set_attributes Thread_Attributes.test_interrupts; val test = Exn.capture Thread.Thread.testInterrupt (); val _ = Thread_Attributes.set_attributes orig_atts; - in Exn.release test end; + in test end; + +val expose_interrupt = Exn.release o expose_interrupt_result; fun try_catch e f = Thread_Attributes.uninterruptible (fn restore_attributes => fn () => diff -r a44ac17ae227 -r eb2255d241da src/Pure/Concurrent/timeout.ML --- a/src/Pure/Concurrent/timeout.ML Mon Sep 25 21:46:38 2023 +0200 +++ b/src/Pure/Concurrent/timeout.ML Mon Sep 25 21:58:58 2023 +0200 @@ -46,7 +46,7 @@ val stop = Time.now (); val was_timeout = not (Event_Timer.cancel request); - val test = Exn.capture Isabelle_Thread.expose_interrupt (); + val test = Isabelle_Thread.expose_interrupt_result (); in if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test) then raise TIMEOUT (stop - start)