# HG changeset patch
# User wenzelm
# Date 1695732153 -7200
# Node ID 909dc00766a011b4a6f9325b6145e5fd09ad3f4e
# Parent  89038d9ef77d8f595c4a3a5a3bb7b329a673045a
clarified signature;

diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/event_timer.ML
--- 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;
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/future.ML
--- 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 *)
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/isabelle_thread.ML
--- 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 ();
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/lazy.ML
--- 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;
 
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/multithreading.ML
--- 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;
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/single_assignment.ML
--- 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;
 
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/synchronized.ML
--- 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);
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/task_queue.ML
--- 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));
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/thread_attributes.ML
--- 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;
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/thread_data.ML
--- 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;
 
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/thread_data_virtual.ML
--- 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;
 
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/unsynchronized.ML
--- 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 *)
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/ML/exn_debugger.ML
--- 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;
 
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/ML/exn_properties.ML
--- 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;
 
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/ML/ml_compiler0.ML
--- 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)};
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/System/command_line.ML
--- 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;
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/System/isabelle_system.ML
--- 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 *)
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/System/scala.ML
--- 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;
 
diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Tools/debugger.ML
--- 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;