--- a/src/Pure/Concurrent/event_timer.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/Concurrent/event_timer.ML Tue Sep 26 12:46:31 2023 +0200
@@ -134,14 +134,14 @@
manager_loop);
fun shutdown () =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn run => fn () =>
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
raise Fail "Concurrent attempt to shutdown event timer"
else (true, make_state (requests, Shutdown_Req, manager_check manager)))
then
- restore_attributes (fn () =>
+ run (fn () =>
Synchronized.guarded_access state
(fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE)) ()
handle exn =>
--- a/src/Pure/Concurrent/future.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Sep 26 12:46:31 2023 +0200
@@ -550,7 +550,7 @@
(* forked results: nested parallel evaluation *)
fun forked_results {name, deps} es =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn run => fn () =>
let
val (group, pri) =
(case worker_task () of
@@ -560,7 +560,7 @@
val futures =
forks {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} es;
in
- restore_attributes join_results futures
+ run join_results futures
handle exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn)
end) ();
--- a/src/Pure/Concurrent/isabelle_thread.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML Tue Sep 26 12:46:31 2023 +0200
@@ -141,13 +141,12 @@
val expose_interrupt = Exn.release o expose_interrupt_result;
fun try_catch e f =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
- restore_attributes e ()
- handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn) ();
+ Thread_Attributes.uninterruptible (fn run => fn () =>
+ 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 restore_attributes => fn () =>
- Exn.release (Exn.capture (restore_attributes e) () before f ())) ();
+ Thread_Attributes.uninterruptible (fn run => fn () =>
+ 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 12:30:08 2023 +0200
+++ b/src/Pure/Concurrent/lazy.ML Tue Sep 26 12:46:31 2023 +0200
@@ -85,7 +85,7 @@
(case peek (Lazy var) of
SOME res => res
| NONE =>
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn run => fn () =>
let
val (expr, x) =
Synchronized.change_result var
@@ -101,7 +101,7 @@
(case expr of
SOME (name, e) =>
let
- val res0 = Exn.capture (restore_attributes e) ();
+ val res0 = Exn.capture (run e) ();
val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
val res = Future.get_result x;
val _ =
@@ -114,7 +114,7 @@
interrupt, until there is a fresh start*)
else Synchronized.change var (fn _ => Expr (name, e));
in res end
- | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
+ | NONE => Exn.capture (run (fn () => Future.join x)) ())
end) ());
end;
--- a/src/Pure/Concurrent/multithreading.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/Concurrent/multithreading.ML Tue Sep 26 12:46:31 2023 +0200
@@ -83,7 +83,7 @@
(* synchronized evaluation *)
fun synchronized name lock e =
- Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Exn.release (Thread_Attributes.uninterruptible (fn run => fn () =>
if ! trace > 0 then
let
val immediate =
@@ -96,14 +96,14 @@
val time = Timer.checkRealTimer timer;
val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
in false end;
- val result = Exn.capture0 (restore_attributes e) ();
+ val result = Exn.capture0 (run e) ();
val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
val _ = Thread.Mutex.unlock lock;
in result end
else
let
val _ = Thread.Mutex.lock lock;
- val result = Exn.capture0 (restore_attributes e) ();
+ val result = Exn.capture0 (run e) ();
val _ = Thread.Mutex.unlock lock;
in result end) ());
--- a/src/Pure/Concurrent/task_queue.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Tue Sep 26 12:46:31 2023 +0200
@@ -156,10 +156,10 @@
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 restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn run => fn () =>
let
val start = Time.now ();
- val result = Exn.capture (restore_attributes e) ();
+ 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) ();
--- a/src/Pure/Concurrent/thread_data.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/Concurrent/thread_data.ML Tue Sep 26 12:46:31 2023 +0200
@@ -30,11 +30,11 @@
fun put (Var tag) data = Thread.Thread.setLocal (tag, data);
fun setmp v data f x =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn run => fn () =>
let
val orig_data = get v;
val _ = put v data;
- val result = Exn.capture0 (restore_attributes f) x;
+ val result = Exn.capture0 (run f) x;
val _ = put v orig_data;
in Exn.release result end) ();
--- a/src/Pure/Concurrent/thread_data_virtual.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/Concurrent/thread_data_virtual.ML Tue Sep 26 12:46:31 2023 +0200
@@ -30,11 +30,11 @@
| SOME x => Inttab.update (i, Universal.tagInject tag x));
fun setmp v data f x =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn run => fn () =>
let
val orig_data = get v;
val _ = put v data;
- val result = Exn.capture (restore_attributes f) x;
+ val result = Exn.capture (run f) x;
val _ = put v orig_data;
in Exn.release result end) ();
--- a/src/Pure/Concurrent/unsynchronized.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML Tue Sep 26 12:46:31 2023 +0200
@@ -39,11 +39,11 @@
fun add i n = (i := ! i + (n: int); ! i);
fun setmp flag value f x =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn run => fn () =>
let
val orig_value = ! flag;
val _ = flag := value;
- val result = Exn.capture0 (restore_attributes f) x;
+ val result = Exn.capture0 (run f) x;
val _ = flag := orig_value;
in Exn.release result end) ();
--- a/src/Pure/General/file_stream.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/General/file_stream.ML Tue Sep 26 12:46:31 2023 +0200
@@ -27,10 +27,10 @@
val platform_path = ML_System.platform_path o Path.implode o Path.expand;
fun with_file open_file close_file f =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn path =>
+ Thread_Attributes.uninterruptible (fn run => fn path =>
let
val file = open_file path;
- val result = Exn.capture (restore_attributes f) file;
+ val result = Exn.capture (run f) file;
in close_file file; Exn.release result end);
in
--- a/src/Pure/General/sha1.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/General/sha1.ML Tue Sep 26 12:46:31 2023 +0200
@@ -155,10 +155,10 @@
(Foreign.cByteArray, Foreign.cUlong, Foreign.cPointer), Foreign.cPointer);
fun with_memory n =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn f =>
+ Thread_Attributes.uninterruptible (fn run => fn f =>
let
val mem = Foreign.Memory.malloc (Word.fromInt n);
- val res = Exn.capture (restore_attributes f) mem;
+ val res = Exn.capture (run f) mem;
val _ = Foreign.Memory.free mem;
in Exn.release res end);
--- a/src/Pure/General/socket_io.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/General/socket_io.ML Tue Sep 26 12:46:31 2023 +0200
@@ -88,10 +88,10 @@
handle OS.SysErr (msg, _) => error (msg ^ ": failed to open socket " ^ socket_name);
fun with_streams f =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn socket_name =>
+ Thread_Attributes.uninterruptible (fn run => fn socket_name =>
let
val streams = open_streams socket_name;
- val result = Exn.capture (restore_attributes f) streams;
+ val result = Exn.capture (run f) streams;
in BinIO.closeIn (#1 streams); BinIO.closeOut (#2 streams); Exn.release result end);
fun with_streams' f socket_name password =
--- a/src/Pure/ML/exn_debugger.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/ML/exn_debugger.ML Tue Sep 26 12:46:31 2023 +0200
@@ -42,10 +42,10 @@
in
fun capture_exception_trace e =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn run => fn () =>
let
val _ = start_trace ();
- val result = Exn.result (restore_attributes e) ();
+ val result = Exn.result (run e) ();
val trace = stop_trace ();
val trace' =
(case result of
--- a/src/Pure/PIDE/query_operation.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/PIDE/query_operation.ML Tue Sep 26 12:46:31 2023 +0200
@@ -19,7 +19,7 @@
Command.print_function (name ^ "_query")
(fn {args = instance :: args, ...} =>
SOME {delay = NONE, pri = pri, persistent = false, strict = false,
- print_fn = fn _ => Thread_Attributes.uninterruptible (fn restore_attributes => fn state =>
+ print_fn = fn _ => Thread_Attributes.uninterruptible (fn run => fn state =>
let
fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
fun status m = output_result (Markup.markup_only m);
@@ -28,11 +28,11 @@
output_result (Markup.markup Markup.error (Runtime.exn_message exn));
val _ = status Markup.running;
- fun run () =
+ fun main () =
f {state = state, args = args, output_result = output_result,
writeln_result = writeln_result};
val _ =
- (case Exn.capture (*sic!*) (restore_attributes run) () of
+ (case Exn.capture (*sic!*) (run main) () of
Exn.Res () => ()
| Exn.Exn exn => toplevel_error exn);
val _ = status Markup.finished;
--- a/src/Pure/System/command_line.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/System/command_line.ML Tue Sep 26 12:46:31 2023 +0200
@@ -13,10 +13,10 @@
struct
fun tool body =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn run => fn () =>
let
val rc =
- (restore_attributes body (); 0) handle exn =>
+ (run body (); 0) handle exn =>
((Runtime.exn_error_message exn; Exn.failure_rc exn) handle err => Exn.failure_rc err);
in exit rc end) ();
--- a/src/Pure/System/isabelle_system.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/System/isabelle_system.ML Tue Sep 26 12:46:31 2023 +0200
@@ -40,7 +40,7 @@
let
val {script, input, cwd, putenv, redirect, timeout, description} =
Bash.dest_params params;
- val run =
+ val server_run =
[Bash.server_run, script, input,
let open XML.Encode in YXML.string_of_body (option (string o absolute_path) cwd) end,
let open XML.Encode in YXML.string_of_body o list (pair string string) end
@@ -59,11 +59,11 @@
with_streams (fn s => Byte_Message.write_message_string (#2 s) [Bash.server_kill, uuid])
| kill NONE = ();
in
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn run => fn () =>
let
fun err () = raise Fail "Malformed result from bash_process server";
fun loop maybe_uuid s =
- (case restore_attributes Byte_Message.read_message_string (#1 s) of
+ (case run Byte_Message.read_message_string (#1 s) of
SOME (head :: args) =>
if head = Bash.server_uuid andalso length args = 1 then
loop (SOME (hd args)) s
@@ -89,7 +89,9 @@
else err ()
| _ => err ())
handle exn => (kill maybe_uuid; Exn.reraise exn);
- in with_streams (fn s => (Byte_Message.write_message_string (#2 s) run; loop NONE s)) end) ()
+ in
+ with_streams (fn s => (Byte_Message.write_message_string (#2 s) server_run; loop NONE s))
+ end) ()
end;
val bash = Bash.script #> bash_process #> Process_Result.print #> Process_Result.rc;
--- a/src/Pure/System/scala.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/System/scala.ML Tue Sep 26 12:46:31 2023 +0200
@@ -42,7 +42,7 @@
in
fun function_bytes name args =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn run => fn () =>
let
val id = new_id ();
fun invoke () =
@@ -60,7 +60,7 @@
| NONE => SOME (Isabelle_Thread.interrupt_exn, tab)));
in
invoke ();
- Exn.release (restore_attributes await_result ())
+ Exn.release (run await_result ())
handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn)
end) ();
--- a/src/Pure/Tools/debugger.ML Tue Sep 26 12:30:08 2023 +0200
+++ b/src/Pure/Tools/debugger.ML Tue Sep 26 12:46:31 2023 +0200
@@ -229,11 +229,11 @@
in
fun debugger_loop thread_name =
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ Thread_Attributes.uninterruptible (fn run => fn () =>
let
fun loop () =
(debugger_state thread_name; if debugger_command thread_name then loop () else ());
- val result = Exn.capture (restore_attributes with_debugging) loop;
+ val result = Exn.capture (run with_debugging) loop;
val _ = debugger_state thread_name;
in Exn.release result end) ();