# HG changeset patch
# User wenzelm
# Date 1695725191 -7200
# Node ID 97dfba4405e3c95ea8994e668796c05402594b6d
# Parent  9506b852ebdf8632cd99fa27d8d65af736a5c074
tuned signature;

diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/Concurrent/event_timer.ML
--- 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 =>
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/Concurrent/future.ML
--- 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) ();
 
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/Concurrent/isabelle_thread.ML
--- 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 ();
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/Concurrent/lazy.ML
--- 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;
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/Concurrent/multithreading.ML
--- 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) ());
 
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/Concurrent/task_queue.ML
--- 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) ();
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/Concurrent/thread_data.ML
--- 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) ();
 
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/Concurrent/thread_data_virtual.ML
--- 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) ();
 
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/Concurrent/unsynchronized.ML
--- 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) ();
 
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/General/file_stream.ML
--- 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
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/General/sha1.ML
--- 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);
 
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/General/socket_io.ML
--- 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 =
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/ML/exn_debugger.ML
--- 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
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/PIDE/query_operation.ML
--- 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;
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/System/command_line.ML
--- 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) ();
 
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/System/isabelle_system.ML
--- 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;
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/System/scala.ML
--- 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) ();
 
diff -r 9506b852ebdf -r 97dfba4405e3 src/Pure/Tools/debugger.ML
--- 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) ();