# HG changeset patch
# User wenzelm
# Date 1697016421 -7200
# Node ID a094bf81a4962dbcd87af04406fec588080ae09c
# Parent  96b3d13606b1c8917223017a3f275ea44934b162
clarified signature;

diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -118,7 +118,7 @@
       (case next_event (Time.now (), ML_Heap.gc_now ()) requests of
         SOME (event, requests') =>
           let
-            val _ = Exn.capture event ();  (*sic!*)
+            val _ = Exn.capture_body event;  (*sic!*)
             val state' = make_state (requests', status, manager);
           in SOME (true, state') end
       | NONE =>
@@ -143,7 +143,7 @@
         fun main () =
           Synchronized.guarded_access state
             (fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE);
-        val result = Exn.capture (run main) ();
+        val result = Exn.capture_body (run main);
       in
         if Exn.is_interrupt_exn result then
           Synchronized.change state (fn State {requests, manager, ...} =>
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -441,9 +441,9 @@
       let
         val res =
           if ok then
-            Exn.capture (fn () =>
+            Exn.capture_body (fn () =>
               Thread_Attributes.with_attributes atts (fn _ =>
-                (Position.setmp_thread_data pos o Context.setmp_generic_context context) e ())) ()
+                (Position.setmp_thread_data pos o Context.setmp_generic_context context) e ()))
           else Isabelle_Thread.interrupt_exn;
       in assign_result group result (identify_result pos res) end;
   in (result, job) end;
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -148,6 +148,7 @@
 struct
   open Exn;
   val capture = capture0;
+  fun capture_body e = capture e ();
 end;
 
 fun expose_interrupt_result () =
@@ -156,7 +157,7 @@
     fun main () =
       (Thread_Attributes.set_attributes Thread_Attributes.test_interrupts;
        Thread.Thread.testInterrupt ());
-    val test = Exn.capture main ();
+    val test = Exn.capture_body main;
     val _ = Thread_Attributes.set_attributes orig_atts;
   in test end;
 
@@ -168,7 +169,7 @@
 
 fun try_finally e f =
   Thread_Attributes.uninterruptible_body (fn run =>
-    Exn.release (Exn.capture (run e) () before f ()));
+    Exn.release (Exn.capture_body (run e) before f ()));
 
 fun try e = Basics.try e ();
 fun can e = Basics.can e ();
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -101,8 +101,8 @@
               (case expr of
                 SOME (name, e) =>
                   let
-                    val res0 = Exn.capture (run e) ();
-                    val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
+                    val res0 = Exn.capture_body (run e);
+                    val _ = Exn.capture_body (fn () => Future.fulfill_result x res0);
                     val res = Future.get_result x;
                     val _ =
                       if not (Exn.is_interrupt_exn res) then
@@ -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 (run (fn () => Future.join x)) ())
+              | NONE => Exn.capture_body (run (fn () => Future.join x)))
             end));
 
 end;
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -159,7 +159,7 @@
   Thread_Attributes.uninterruptible_body (fn run =>
     let
       val start = Time.now ();
-      val result = Exn.capture (run e) ();
+      val result = Exn.capture_body (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 96b3d13606b1 -r a094bf81a496 src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/timeout.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -42,7 +42,7 @@
           Event_Timer.request {physical = physical} (start + scale_time timeout)
             (fn () => Isabelle_Thread.interrupt_other self);
         val result =
-          Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
+          Exn.capture_body (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x));
 
         val stop = Time.now ();
         val was_timeout = not (Event_Timer.cancel request);
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/General/exn.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -39,6 +39,7 @@
 sig
   include EXN0
   val capture: ('a -> 'b) -> 'a -> 'b result  (*managed interrupts*)
+  val capture_body: (unit -> 'a) -> 'a result
 end;
 
 structure Exn: EXN0 =
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -331,7 +331,7 @@
 in
 
 fun apply_capture int name markers trans state =
-  (case Exn.capture (fn () => apply_body int trans state |> apply_markers name markers) () of
+  (case Exn.capture_body (fn () => apply_body int trans state |> apply_markers name markers) of
     Exn.Res res => res
   | Exn.Exn exn => (state, SOME exn));
 
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -550,7 +550,7 @@
           (fn deps => fn (name, node) =>
             if Symset.member required name orelse visible_node node orelse pending_result node then
               let
-                fun body () =
+                fun main () =
                  (Execution.worker_task_active true name;
                   if forall finished_import deps then
                     iterate_entries (fn (_, opt_exec) => fn () =>
@@ -569,7 +569,7 @@
                     deps = delay :: Execution.active_tasks name @ maps (the_list o #2 o #2) deps,
                     pri = 0, interrupts = false}
                   (fn () =>
-                    (case Exn.capture body () of
+                    (case Exn.capture_body main of
                       Exn.Res () => ()
                     | Exn.Exn exn =>
                        (Output.system_message (Runtime.exn_message exn);
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/PIDE/execution.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -165,11 +165,11 @@
               val task = the (Future.worker_task ());
               val _ = status task [Markup.running];
               val result =
-                Exn.capture (Future.interruptible_task e) ()
+                Exn.capture_body (Future.interruptible_task e)
                 |> Future.identify_result pos
                 |> Exn.map_exn Runtime.thread_context;
               val errors =
-                Exn.capture (fn () =>
+                Exn.capture_body (fn () =>
                   (case result of
                     Exn.Exn exn =>
                      (status task [Markup.failed];
@@ -178,7 +178,7 @@
                       if exec_id = 0 then ()
                       else List.app (Future.error_message pos) (Runtime.exn_messages exn))
                   | Exn.Res _ =>
-                      status task [Markup.finished])) ();
+                      status task [Markup.finished]));
               val _ = status task [Markup.joined];
             in Exn.release errors; Exn.release result end);
 
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/PIDE/protocol.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -164,7 +164,7 @@
 val _ =
   Protocol_Command.define "Document.dialog_result"
     (fn [serial, result] =>
-      (case Exn.capture (fn () => Active.dialog_result (Value.parse_int serial) result) () of
+      (case Exn.capture_body (fn () => Active.dialog_result (Value.parse_int serial) result) of
         Exn.Res () => ()
       | Exn.Exn exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn));
 
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/PIDE/protocol_command.ML
--- a/src/Pure/PIDE/protocol_command.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/PIDE/protocol_command.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -40,7 +40,7 @@
   (case Symtab.lookup (Synchronized.value commands) name of
     NONE => error ("Undefined Isabelle protocol command " ^ quote name)
   | SOME cmd =>
-      (case Exn.capture (fn () => Runtime.exn_trace_system (fn () => cmd args)) () of
+      (case Exn.capture_body (fn () => Runtime.exn_trace_system (fn () => cmd args)) of
         Exn.Res res => res
       | Exn.Exn exn =>
           if is_protocol_exn exn then Exn.reraise exn
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/PIDE/query_operation.ML
--- a/src/Pure/PIDE/query_operation.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/PIDE/query_operation.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -32,7 +32,7 @@
               f {state = state, args = args, output_result = output_result,
                   writeln_result = writeln_result};
             val _ =
-              (case Exn.capture (*sic!*) (run main) () of
+              (case Exn.capture_body (*sic!*) (run main) of
                 Exn.Res () => ()
               | Exn.Exn exn => toplevel_error exn);
             val _ = status Markup.finished;
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/System/command_line.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -12,12 +12,12 @@
 structure Command_Line: COMMAND_LINE =
 struct
 
-fun tool body =
+fun tool main =
   Thread_Attributes.uninterruptible_body (fn run =>
     let
       fun print_failure exn = (Runtime.exn_error_message exn; Exn.failure_rc exn);
       val rc =
-        (case Exn.capture (run body) () of
+        (case Exn.capture_body (run main) of
           Exn.Res () => 0
         | Exn.Exn exn =>
             (case Exn.capture print_failure exn of
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -154,13 +154,13 @@
 
     fun protocol_loop () =
       let
-        fun body () =
+        fun main () =
           (case Byte_Message.read_message in_stream of
             NONE => raise Protocol_Command.STOP 0
           | SOME [] => Output.system_message "Isabelle process: no input"
           | SOME (name :: args) => Protocol_Command.run (Bytes.content name) args);
         val _ =
-          (case Exn.capture body () of
+          (case Exn.capture_body main of
             Exn.Res () => ()
           | Exn.Exn exn =>
               if Protocol_Command.is_protocol_exn exn then Exn.reraise exn
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/System/isabelle_system.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -89,7 +89,7 @@
                else err ()
           | _ => err ())
         and loop maybe_uuid s =
-          (case Exn.capture (fn () => loop_body s) () of
+          (case Exn.capture_body (fn () => loop_body s) of
             Exn.Res res => res
           | Exn.Exn exn => (kill maybe_uuid; Exn.reraise exn));
       in
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/System/scala.ML
--- a/src/Pure/System/scala.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/System/scala.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -60,7 +60,7 @@
             | NONE => SOME (Isabelle_Thread.interrupt_exn, tab)));
     in
       invoke ();
-      (case Exn.capture (fn () => Exn.release (run await_result ())) () of
+      (case Exn.capture_body (fn () => Exn.release (run await_result ())) of
         Exn.Res res => res
       | Exn.Exn exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn))
     end);
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -225,7 +225,7 @@
       (case present () of
         NONE => []
       | SOME (context as {segments, ...}) =>
-          [Exn.capture (fn () => (apply_presentation context theory; (theory, segments))) ()]);
+          [Exn.capture_body (fn () => (apply_presentation context theory; (theory, segments)))]);
 
 in
 
@@ -247,7 +247,7 @@
                   deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
                 (fn () => body (join_parents deps name parents))
             else
-              Future.value_result (Exn.capture (fn () => body (join_parents deps name parents)) ())
+              Future.value_result (Exn.capture_body (fn () => body (join_parents deps name parents)))
         | Finished theory => Future.value (theory_result theory)));
 
     val results1 = futures |> maps (consolidate_theory o Future.join_result);
@@ -256,7 +256,7 @@
     val results2 = (map o Exn.map_res) (K ()) present_results;
 
     val results3 = futures
-      |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
+      |> map (fn future => Exn.capture_body (fn () => result_commit (Future.join future) ()));
 
     val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
 
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Tools/build.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -91,7 +91,7 @@
                   Exn.Res loaded_theories =>
                     Exn.capture (apply_hooks session_name) (flat loaded_theories)
                 | Exn.Exn exn => Exn.Exn exn);
-              val res2 = Exn.capture Session.finish ();
+              val res2 = Exn.capture_body Session.finish;
 
               val _ = Resources.finish_session_base ();
               val _ = Par_Exn.release_all [res1, res2];
@@ -107,7 +107,7 @@
             else e ();
         in
           exec (fn () =>
-            (case Exn.capture (Future.interruptible_task build) () of
+            (case Exn.capture_body (Future.interruptible_task build) of
               Exn.Res () => (0, [])
             | Exn.Exn exn =>
                 (case Exn.capture Runtime.exn_message_list exn of
diff -r 96b3d13606b1 -r a094bf81a496 src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -414,7 +414,7 @@
         end
     in
       fn [serial_string, reply] =>
-        (case Exn.capture (fn () => body serial_string reply) () of
+        (case Exn.capture_body (fn () => body serial_string reply) of
           Exn.Res () => ()
         | Exn.Exn exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn)
     end;