# HG changeset patch # User wenzelm # Date 1695332703 -7200 # Node ID 38fe769658be7308f90d2bd63c76702b17407746 # Parent 61a6b4b81d6eb079210e59665aa9d1f02e42afeb clarified modules; clarified signature; diff -r 61a6b4b81d6e -r 38fe769658be src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Thu Sep 21 18:17:26 2023 +0200 +++ b/src/Doc/Implementation/ML.thy Thu Sep 21 23:45:03 2023 +0200 @@ -1121,7 +1121,8 @@ text \ These indicate arbitrary system events: both the ML runtime system and the Isabelle/ML infrastructure signal various exceptional situations by raising - the special \<^ML>\Exn.Interrupt\ exception in user code. + special exceptions user code, satisfying the predicate + \<^ML>\Exn.is_interrupt\. This is the one and only way that physical events can intrude an Isabelle/ML program. Such an interrupt can mean out-of-memory, stack overflow, timeout, diff -r 61a6b4b81d6e -r 38fe769658be src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Sep 21 18:17:26 2023 +0200 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Sep 21 23:45:03 2023 +0200 @@ -1049,7 +1049,7 @@ in if not (null ps) orelse rc = 0 then Normal (ps, js, first_error) else if rc = 2 then TimedOut js - else if rc = 130 then Exn.interrupt () + else if rc = 130 then Isabelle_Thread.interrupt_self () else Error (if first_error = "" then "Unknown error" else first_error, js) end end diff -r 61a6b4b81d6e -r 38fe769658be src/HOL/Tools/Sledgehammer/async_manager_legacy.ML --- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Thu Sep 21 18:17:26 2023 +0200 +++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Thu Sep 21 23:45:03 2023 +0200 @@ -102,7 +102,7 @@ NONE else let - val _ = List.app (Isabelle_Thread.interrupt_unsynchronized o #1) canceling + val _ = List.app (Isabelle_Thread.interrupt_other o #1) canceling val canceling' = filter (Isabelle_Thread.is_active o #1) canceling val state' = make_state manager timeout_heap' active canceling' messages in SOME (map #2 timeout_threads, state') end diff -r 61a6b4b81d6e -r 38fe769658be src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Thu Sep 21 18:17:26 2023 +0200 +++ b/src/Pure/Concurrent/future.ML Thu Sep 21 23:45:03 2023 +0200 @@ -195,13 +195,13 @@ val running = Task_Queue.cancel (! queue) group; val _ = running |> List.app (fn thread => if Isabelle_Thread.is_self thread then () - else Isabelle_Thread.interrupt_unsynchronized thread); + else Isabelle_Thread.interrupt_other thread); in running end; fun cancel_all () = (*requires SYNCHRONIZED*) let val (groups, threads) = Task_Queue.cancel_all (! queue); - val _ = List.app Isabelle_Thread.interrupt_unsynchronized threads; + val _ = List.app Isabelle_Thread.interrupt_other threads; in groups end; fun cancel_later group = (*requires SYNCHRONIZED*) @@ -450,7 +450,7 @@ Exn.capture (fn () => Thread_Attributes.with_attributes atts (fn _ => (Position.setmp_thread_data pos o Context.setmp_generic_context context) e ())) () - else Exn.interrupt_exn; + else Isabelle_Thread.interrupt_exn; in assign_result group result (identify_result pos res) end; in (result, job) end; @@ -645,7 +645,7 @@ let val group = worker_subgroup (); val result = Single_Assignment.var "promise" : 'a result; - fun assign () = assign_result group result Exn.interrupt_exn + fun assign () = assign_result group result Isabelle_Thread.interrupt_exn handle Fail _ => true | exn => if Exn.is_interrupt exn @@ -665,7 +665,8 @@ val group = Task_Queue.group_of_task task; val pos = Position.thread_data (); fun job ok = - assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn); + assign_result group result + (if ok then identify_result pos res else Isabelle_Thread.interrupt_exn); val _ = Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn _ => let diff -r 61a6b4b81d6e -r 38fe769658be src/Pure/Concurrent/isabelle_thread.ML --- a/src/Pure/Concurrent/isabelle_thread.ML Thu Sep 21 18:17:26 2023 +0200 +++ b/src/Pure/Concurrent/isabelle_thread.ML Thu Sep 21 23:45:03 2023 +0200 @@ -20,7 +20,10 @@ val fork: params -> (unit -> unit) -> T val is_active: T -> bool val join: T -> unit - val interrupt_unsynchronized: T -> unit + val interrupt: exn + val interrupt_exn: 'a Exn.result + val interrupt_self: unit -> 'a + val interrupt_other: T -> unit end; structure Isabelle_Thread: ISABELLE_THREAD = @@ -102,9 +105,14 @@ do OS.Process.sleep (seconds 0.1); -(* interrupt *) +(* interrupts *) -fun interrupt_unsynchronized t = +val interrupt = Thread.Thread.Interrupt; +val interrupt_exn = Exn.Exn interrupt; + +fun interrupt_self () = raise interrupt; + +fun interrupt_other t = Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => (); end; diff -r 61a6b4b81d6e -r 38fe769658be src/Pure/Concurrent/par_exn.ML --- a/src/Pure/Concurrent/par_exn.ML Thu Sep 21 18:17:26 2023 +0200 +++ b/src/Pure/Concurrent/par_exn.ML Thu Sep 21 23:45:03 2023 +0200 @@ -21,7 +21,7 @@ exception Par_Exn of exn list; (*non-empty list with unique identified elements sorted by Exn_Properties.ord; - no occurrences of Par_Exn or Exn.Interrupt*) + no occurrences of Par_Exn or Exn.is_interrupt*) fun par_exns (Par_Exn exns) = exns | par_exns exn = if Exn.is_interrupt exn then [] else [Exn_Properties.identify [] exn]; @@ -30,7 +30,7 @@ let val exnss = map par_exns exns; val exns' = Ord_List.unions Exn_Properties.ord exnss handle Option.Option => flat exnss; - in if null exns' then Exn.Interrupt else Par_Exn exns' end; + in if null exns' then Isabelle_Thread.interrupt else Par_Exn exns' end; fun dest (Par_Exn exns) = SOME exns | dest exn = if Exn.is_interrupt exn then SOME [] else NONE; diff -r 61a6b4b81d6e -r 38fe769658be src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Thu Sep 21 18:17:26 2023 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Thu Sep 21 23:45:03 2023 +0200 @@ -296,7 +296,7 @@ fun cancel (Queue {groups, jobs, ...}) group = let - val _ = cancel_group group Exn.Interrupt; + val _ = cancel_group group Isabelle_Thread.interrupt; val running = Tasks.fold (fn task => (case get_job jobs task of Running thread => insert Isabelle_Thread.equal thread | _ => I)) @@ -308,7 +308,7 @@ fun cancel_job (task, (job, _)) (groups, running) = let val group = group_of_task task; - val _ = cancel_group group Exn.Interrupt; + val _ = cancel_group group Isabelle_Thread.interrupt; in (case job of Running t => (insert eq_group group groups, insert Isabelle_Thread.equal t running) diff -r 61a6b4b81d6e -r 38fe769658be src/Pure/Concurrent/timeout.ML --- a/src/Pure/Concurrent/timeout.ML Thu Sep 21 18:17:26 2023 +0200 +++ b/src/Pure/Concurrent/timeout.ML Thu Sep 21 23:45:03 2023 +0200 @@ -40,7 +40,7 @@ val request = Event_Timer.request {physical = physical} (start + scale_time timeout) - (fn () => Isabelle_Thread.interrupt_unsynchronized self); + (fn () => Isabelle_Thread.interrupt_other self); val result = Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) (); diff -r 61a6b4b81d6e -r 38fe769658be src/Pure/General/exn.ML --- a/src/Pure/General/exn.ML Thu Sep 21 18:17:26 2023 +0200 +++ b/src/Pure/General/exn.ML Thu Sep 21 23:45:03 2023 +0200 @@ -26,10 +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 - exception Interrupt - val interrupt: unit -> 'a val is_interrupt: exn -> bool - val interrupt_exn: 'a result val is_interrupt_exn: 'a result -> bool val interruptible_capture: ('a -> 'b) -> 'a -> 'b result val failure_rc: exn -> int @@ -92,16 +89,10 @@ (* interrupts *) -exception Interrupt = Thread.Thread.Interrupt; - -fun interrupt () = raise Interrupt; - -fun is_interrupt Interrupt = true +fun is_interrupt Thread.Thread.Interrupt = true | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause | is_interrupt _ = false; -val interrupt_exn = Exn Interrupt; - fun is_interrupt_exn (Exn exn) = is_interrupt exn | is_interrupt_exn _ = false; diff -r 61a6b4b81d6e -r 38fe769658be src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Thu Sep 21 18:17:26 2023 +0200 +++ b/src/Pure/PIDE/command.ML Thu Sep 21 23:45:03 2023 +0200 @@ -241,7 +241,9 @@ let val _ = status tr Markup.failed; val _ = status tr Markup.finished; - val _ = if null errs then (status tr Markup.canceled; Exn.interrupt ()) else (); + val _ = + if null errs then (status tr Markup.canceled; Isabelle_Thread.interrupt_self ()) + else (); in {failed = true, command = tr, state = st} end | SOME st' => let diff -r 61a6b4b81d6e -r 38fe769658be src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Thu Sep 21 18:17:26 2023 +0200 +++ b/src/Pure/System/isabelle_system.ML Thu Sep 21 23:45:03 2023 +0200 @@ -68,7 +68,7 @@ if head = Bash.server_uuid andalso length args = 1 then loop (SOME (hd args)) s else if head = Bash.server_interrupt andalso null args then - Exn.interrupt () + Isabelle_Thread.interrupt_self () else if head = Bash.server_failure andalso length args = 1 then raise Fail (hd args) else if head = Bash.server_result andalso length args >= 4 then diff -r 61a6b4b81d6e -r 38fe769658be src/Pure/System/scala.ML --- a/src/Pure/System/scala.ML Thu Sep 21 18:17:26 2023 +0200 +++ b/src/Pure/System/scala.ML Thu Sep 21 23:45:03 2023 +0200 @@ -35,7 +35,7 @@ | ("1", _) => Exn.Res rest | ("2", [msg]) => Exn.Exn (ERROR (Bytes.content msg)) | ("3", [msg]) => Exn.Exn (Fail (Bytes.content msg)) - | ("4", []) => Exn.interrupt_exn + | ("4", []) => Isabelle_Thread.interrupt_exn | _ => raise Fail "Malformed Scala.result"); in Synchronized.change results (Symtab.map_entry (Bytes.content id) (K result)) end); @@ -57,7 +57,7 @@ (case Symtab.lookup tab id of SOME (Exn.Exn Match) => NONE | SOME result => SOME (result, Symtab.delete id tab) - | NONE => SOME (Exn.interrupt_exn, tab))); + | NONE => SOME (Isabelle_Thread.interrupt_exn, tab))); in invoke (); Exn.release (restore_attributes await_result ())