--- a/src/Pure/Concurrent/event_timer.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/event_timer.ML Tue Sep 26 14:42:33 2023 +0200
@@ -134,7 +134,7 @@
manager_loop);
fun shutdown () =
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
if Synchronized.change_result state (fn st as State {requests, manager, ...} =>
if is_shutdown Normal st then (false, st)
else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then
@@ -149,7 +149,7 @@
Synchronized.change state (fn State {requests, manager, ...} =>
make_state (requests, Normal, manager))
else ()
- else ()) ();
+ else ());
(* main operations *)
@@ -170,12 +170,12 @@
in (canceled, make_state (requests', status, manager')) end);
fun future physical time =
- Thread_Attributes.uninterruptible (fn _ => fn () =>
+ Thread_Attributes.uninterruptible_body (fn _ =>
let
val req: request Single_Assignment.var = Single_Assignment.var "req";
fun abort () = ignore (cancel (Single_Assignment.await req));
val promise: unit future = Future.promise_name "event_timer" abort;
val _ = Single_Assignment.assign req (request physical time (Future.fulfill promise));
- in promise end) ();
+ in promise end);
end;
--- a/src/Pure/Concurrent/future.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Sep 26 14:42:33 2023 +0200
@@ -550,7 +550,7 @@
(* forked results: nested parallel evaluation *)
fun forked_results {name, deps} es =
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val (group, pri) =
(case worker_task () of
@@ -562,7 +562,7 @@
in
run join_results futures
handle exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn)
- end) ();
+ end);
(* task context for running thread *)
--- a/src/Pure/Concurrent/isabelle_thread.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML Tue Sep 26 14:42:33 2023 +0200
@@ -141,12 +141,12 @@
val expose_interrupt = Exn.release o expose_interrupt_result;
fun try_catch e f =
- Thread_Attributes.uninterruptible (fn run => fn () =>
- run e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn) ();
+ Thread_Attributes.uninterruptible_body (fn run =>
+ run e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn);
fun try_finally e f =
- Thread_Attributes.uninterruptible (fn run => fn () =>
- Exn.release (Exn.capture (run e) () before f ())) ();
+ Thread_Attributes.uninterruptible_body (fn run =>
+ Exn.release (Exn.capture (run e) () before f ()));
fun try e = Basics.try e ();
fun can e = Basics.can e ();
--- a/src/Pure/Concurrent/lazy.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/lazy.ML Tue Sep 26 14:42:33 2023 +0200
@@ -85,7 +85,7 @@
(case peek (Lazy var) of
SOME res => res
| NONE =>
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val (expr, x) =
Synchronized.change_result var
@@ -115,7 +115,7 @@
else Synchronized.change var (fn _ => Expr (name, e));
in res end
| NONE => Exn.capture (run (fn () => Future.join x)) ())
- end) ());
+ end));
end;
--- a/src/Pure/Concurrent/multithreading.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/multithreading.ML Tue Sep 26 14:42:33 2023 +0200
@@ -67,9 +67,9 @@
fun tracing level msg =
if ! trace < level then ()
- else Thread_Attributes.uninterruptible (fn _ => fn () =>
+ else Thread_Attributes.uninterruptible_body (fn _ =>
(TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
- handle _ (*sic*) => ()) ();
+ handle _ (*sic*) => ());
fun tracing_time detailed time =
tracing
@@ -83,7 +83,7 @@
(* synchronized evaluation *)
fun synchronized name lock e =
- Exn.release (Thread_Attributes.uninterruptible (fn run => fn () =>
+ Exn.release (Thread_Attributes.uninterruptible_body (fn run =>
if ! trace > 0 then
let
val immediate =
@@ -105,6 +105,6 @@
val _ = Thread.Mutex.lock lock;
val result = Exn.capture0 (run e) ();
val _ = Thread.Mutex.unlock lock;
- in result end) ());
+ in result end));
end;
--- a/src/Pure/Concurrent/single_assignment.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML Tue Sep 26 14:42:33 2023 +0200
@@ -61,9 +61,9 @@
(case ! state of
Set _ => assign_fail name
| Unset _ =>
- Thread_Attributes.uninterruptible (fn _ => fn () =>
+ Thread_Attributes.uninterruptible_body (fn _ =>
(state := Set x; RunCall.clearMutableBit state;
- Thread.ConditionVar.broadcast cond)) ())));
+ Thread.ConditionVar.broadcast cond)))));
end;
--- a/src/Pure/Concurrent/synchronized.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Tue Sep 26 14:42:33 2023 +0200
@@ -57,9 +57,9 @@
(case ! state of
Immutable _ => immutable_fail name
| Mutable _ =>
- Thread_Attributes.uninterruptible (fn _ => fn () =>
+ Thread_Attributes.uninterruptible_body (fn _ =>
(state := Immutable x; RunCall.clearMutableBit state;
- Thread.ConditionVar.broadcast cond)) ())));
+ Thread.ConditionVar.broadcast cond)))));
(* synchronized access *)
@@ -81,9 +81,9 @@
| Exn.Res false => NONE
| Exn.Exn exn => Exn.reraise exn)
| SOME (y, x') =>
- Thread_Attributes.uninterruptible (fn _ => fn () =>
+ Thread_Attributes.uninterruptible_body (fn _ =>
(state := Mutable {lock = lock, cond = cond, content = x'};
- Thread.ConditionVar.broadcast cond; SOME y)) ()));
+ Thread.ConditionVar.broadcast cond; SOME y))));
in try_change () end));
fun guarded_access var f = the (timed_access var (fn _ => NONE) f);
--- a/src/Pure/Concurrent/task_queue.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Tue Sep 26 14:42:33 2023 +0200
@@ -156,13 +156,13 @@
fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
fun update_timing update (Task {timing, ...}) e =
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val start = Time.now ();
val result = Exn.capture (run e) ();
val t = Time.now () - start;
val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
- in Exn.release result end) ();
+ in Exn.release result end);
fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
--- a/src/Pure/Concurrent/thread_attributes.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/thread_attributes.ML Tue Sep 26 14:42:33 2023 +0200
@@ -18,6 +18,7 @@
val safe_interrupts: attributes -> attributes
val with_attributes: attributes -> (attributes -> 'a) -> 'a
val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
+ val uninterruptible_body: ((('b -> 'c) -> 'b -> 'c) -> 'a) -> 'a
end;
structure Thread_Attributes: THREAD_ATTRIBUTES =
@@ -106,4 +107,7 @@
with_attributes no_interrupts (fn atts =>
f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
+fun uninterruptible_body body =
+ uninterruptible (fn run => fn () => body run) ();
+
end;
--- a/src/Pure/Concurrent/thread_data.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/thread_data.ML Tue Sep 26 14:42:33 2023 +0200
@@ -30,13 +30,13 @@
fun put (Var tag) data = Thread.Thread.setLocal (tag, data);
fun setmp v data f x =
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val orig_data = get v;
val _ = put v data;
val result = Exn.capture0 (run f) x;
val _ = put v orig_data;
- in Exn.release result end) ();
+ in Exn.release result end);
end;
--- a/src/Pure/Concurrent/thread_data_virtual.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/thread_data_virtual.ML Tue Sep 26 14:42:33 2023 +0200
@@ -30,13 +30,13 @@
| SOME x => Inttab.update (i, Universal.tagInject tag x));
fun setmp v data f x =
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val orig_data = get v;
val _ = put v data;
val result = Exn.capture (run f) x;
val _ = put v orig_data;
- in Exn.release result end) ();
+ in Exn.release result end);
end;
--- a/src/Pure/Concurrent/unsynchronized.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML Tue Sep 26 14:42:33 2023 +0200
@@ -39,13 +39,13 @@
fun add i n = (i := ! i + (n: int); ! i);
fun setmp flag value f x =
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val orig_value = ! flag;
val _ = flag := value;
val result = Exn.capture0 (run f) x;
val _ = flag := orig_value;
- in Exn.release result end) ();
+ in Exn.release result end);
(* weak references *)
--- a/src/Pure/ML/exn_debugger.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/ML/exn_debugger.ML Tue Sep 26 14:42:33 2023 +0200
@@ -42,7 +42,7 @@
in
fun capture_exception_trace e =
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val _ = start_trace ();
val result = Exn.result (run e) ();
@@ -54,7 +54,7 @@
trace
|> map_filter (fn (entry, e) => if eq_exn (exn, e) then SOME entry else NONE)
|> rev);
- in (trace', result) end) ();
+ in (trace', result) end);
end;
--- a/src/Pure/ML/exn_properties.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/ML/exn_properties.ML Tue Sep 26 14:42:33 2023 +0200
@@ -63,8 +63,8 @@
startLine = #startLine loc, endLine = #endLine loc,
startPosition = #startPosition loc, endPosition = #endPosition loc};
in
- Thread_Attributes.uninterruptible (fn _ => fn () =>
- PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
+ Thread_Attributes.uninterruptible_body (fn _ =>
+ PolyML.raiseWithLocation (exn, loc') handle exn' => exn')
end
end;
--- a/src/Pure/ML/ml_compiler0.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/ML/ml_compiler0.ML Tue Sep 26 14:42:33 2023 +0200
@@ -117,12 +117,12 @@
end;
-fun ML_file context {verbose, debug} file = Thread_Attributes.uninterruptible (fn run => fn () =>
+fun ML_file context {verbose, debug} file = Thread_Attributes.uninterruptible_body (fn run =>
let
val instream = TextIO.openIn file;
val result = Exn.capture (run TextIO.inputAll) instream;
val _ = TextIO.closeIn instream;
- in ML context {line = 1, file = file, verbose = verbose, debug = debug} (Exn.release result) end) ();
+ in ML context {line = 1, file = file, verbose = verbose, debug = debug} (Exn.release result) end);
fun ML_file_operations (f: bool option -> string -> unit) =
{ML_file = f NONE, ML_file_debug = f (SOME true), ML_file_no_debug = f (SOME false)};
--- a/src/Pure/System/command_line.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/System/command_line.ML Tue Sep 26 14:42:33 2023 +0200
@@ -13,11 +13,11 @@
struct
fun tool body =
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val rc =
(run body (); 0) handle exn =>
((Runtime.exn_error_message exn; Exn.failure_rc exn) handle err => Exn.failure_rc err);
- in exit rc end) ();
+ in exit rc end);
end;
--- a/src/Pure/System/isabelle_system.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/System/isabelle_system.ML Tue Sep 26 14:42:33 2023 +0200
@@ -59,7 +59,7 @@
with_streams (fn s => Byte_Message.write_message_string (#2 s) [Bash.server_kill, uuid])
| kill NONE = ();
in
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
fun err () = raise Fail "Malformed result from bash_process server";
fun loop maybe_uuid s =
@@ -91,7 +91,7 @@
handle exn => (kill maybe_uuid; Exn.reraise exn);
in
with_streams (fn s => (Byte_Message.write_message_string (#2 s) server_run; loop NONE s))
- end) ()
+ end)
end;
val bash = Bash.script #> bash_process #> Process_Result.print #> Process_Result.rc;
@@ -149,13 +149,13 @@
fun rm_tree path = scala_function "rm_tree" [path];
-fun with_tmp_dir name f = Thread_Attributes.uninterruptible (fn run => fn () =>
+fun with_tmp_dir name f = Thread_Attributes.uninterruptible_body (fn run =>
let
val path = create_tmp_path name "";
val _ = make_directory path;
val result = Exn.capture (run f) path;
val _ = try rm_tree path;
- in Exn.release result end) ();
+ in Exn.release result end);
(* download file *)
--- a/src/Pure/System/scala.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/System/scala.ML Tue Sep 26 14:42:33 2023 +0200
@@ -42,7 +42,7 @@
in
fun function_bytes name args =
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val id = new_id ();
fun invoke () =
@@ -62,7 +62,7 @@
invoke ();
Exn.release (run await_result ())
handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn)
- end) ();
+ end);
val function1_bytes = singleton o function_bytes;
--- a/src/Pure/Tools/debugger.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Tools/debugger.ML Tue Sep 26 14:42:33 2023 +0200
@@ -229,13 +229,13 @@
in
fun debugger_loop thread_name =
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
fun loop () =
(debugger_state thread_name; if debugger_command thread_name then loop () else ());
val result = Exn.capture (run with_debugging) loop;
val _ = debugger_state thread_name;
- in Exn.release result end) ();
+ in Exn.release result end);
end;