clarified signature: avoid association with potentially dangerous Exn.capture;

--- a/src/Doc/Implementation/ML.thy	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Doc/Implementation/ML.thy	Mon Sep 25 18:45:41 2023 +0200
@@ -1958,7 +1958,7 @@
   \begin{mldecls}
   @{define_ML_type 'a "Exn.result"} \\
   @{define_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
-  @{define_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
+  @{define_ML Exn.result: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
   @{define_ML Exn.release: "'a Exn.result -> 'a"} \\
   @{define_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\
   @{define_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\
@@ -1973,8 +1973,8 @@
   precautions apply to user code: interrupts must not be absorbed
   accidentally!
 
-  \<^descr> \<^ML>\<open>Exn.interruptible_capture\<close> is similar to \<^ML>\<open>Exn.capture\<close>, but
-  interrupts are immediately re-raised as required for user code.
+  \<^descr> \<^ML>\<open>Exn.result\<close> is similar to \<^ML>\<open>Exn.capture\<close>, but interrupts are
+  immediately re-raised as required for user code.
 
   \<^descr> \<^ML>\<open>Exn.release\<close>~\<open>result\<close> releases the original runtime result, exposing
   its regular value or raising the reified exception.

--- a/src/HOL/Library/code_test.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/HOL/Library/code_test.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -157,8 +157,7 @@
         (driver ctxt ((apfst o map) (apfst Long_Name.implode #> apsnd Bytes.content) result))
       |> parse_result compiler
     fun evaluator program _ vs_ty deps =
-      Exn.interruptible_capture eval
-        (Code_Target.compilation_text ctxt target program deps true vs_ty)
+      Exn.result eval (Code_Target.compilation_text ctxt target program deps true vs_ty)
     fun postproc f = map (apsnd (Option.map (map f)))
   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
 

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -315,7 +315,7 @@
 fun dynamic_value_strict opts cookie ctxt postproc t =
   let
     fun evaluator program _ vs_ty_t deps =
-      Exn.interruptible_capture (value opts ctxt cookie)
+      Exn.result (value opts ctxt cookie)
         (Code_Target.compilation_text ctxt target program deps true vs_ty_t)
   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
 

--- a/src/Pure/Concurrent/future.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -614,10 +614,10 @@
 
 fun cond_forks args es =
   if enabled () then forks args es
-  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
+  else map (fn e => value_result (Exn.result e ())) es;
 
 fun map_future f x =
-  if is_finished x then value_result (Exn.interruptible_capture (f o join) x)
+  if is_finished x then value_result (Exn.result (f o join) x)
   else
     let
       val task = task_of x;

--- a/src/Pure/Concurrent/par_list.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -37,7 +37,7 @@
 
 fun map' params f xs = Par_Exn.release_first (managed_results params f xs);
 fun map f = map' {name = "", sequential = false} f;
-fun map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all;
+fun map_independent f = map (Exn.result f) #> Par_Exn.release_all;
 
 fun get_some f xs =
   let

--- a/src/Pure/General/exn.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Pure/General/exn.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -29,7 +29,7 @@
   val cause: exn -> exn
   val is_interrupt: exn -> bool
   val is_interrupt_exn: 'a result -> bool
-  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
+  val result: ('a -> 'b) -> 'a -> 'b result
   val failure_rc: exn -> int
   exception EXCEPTIONS of exn list
   val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
@@ -101,7 +101,7 @@
 fun is_interrupt_exn (Exn exn) = is_interrupt exn
   | is_interrupt_exn _ = false;
 
-fun interruptible_capture f x =
+fun result f x =
   Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
 
 fun failure_rc exn = if is_interrupt exn then 130 else 2;

--- a/src/Pure/General/exn.scala	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Pure/General/exn.scala	Mon Sep 25 18:45:41 2023 +0200
@@ -93,7 +93,7 @@
       case _ => false
     }
 
-  def interruptible_capture[A](e: => A): Result[A] =
+  def result[A](e: => A): Result[A] =
     try { Res(e) }
     catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) }
 

--- a/src/Pure/General/timing.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Pure/General/timing.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -90,7 +90,7 @@
 fun cond_timeit enabled msg e =
   if enabled then
     let
-      val (t, result) = timing (Exn.interruptible_capture e) ();
+      val (t, result) = timing (Exn.result e) ();
       val _ =
         if is_relevant t then
           let val end_msg = message t
@@ -111,7 +111,7 @@
 
 fun protocol name pos f x =
   let
-    val (t, result) = timing (Exn.interruptible_capture f) x;
+    val (t, result) = timing (Exn.result f) x;
     val _ = protocol_message name pos t;
   in Exn.release result end;
 

--- a/src/Pure/Isar/proof.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -1259,7 +1259,7 @@
     val test_proof =
       local_skip_proof true
       |> Unsynchronized.setmp testing true
-      |> Exn.interruptible_capture;
+      |> Exn.result;
 
     fun after_qed' (result_ctxt, results) state' = state'
       |> refine_goals print_rule result_ctxt (flat results)

--- a/src/Pure/ML/exn_debugger.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Pure/ML/exn_debugger.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -45,7 +45,7 @@
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val _ = start_trace ();
-      val result = Exn.interruptible_capture (restore_attributes e) ();
+      val result = Exn.result (restore_attributes e) ();
       val trace = stop_trace ();
       val trace' =
         (case result of

--- a/src/Pure/PIDE/command.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -81,7 +81,7 @@
                   let val _ = Position.report pos (Markup.language_path delimited) in
                     case content of
                       NONE =>
-                        Exn.interruptible_capture (fn () =>
+                        Exn.result (fn () =>
                           Resources.read_file_node file_node master_dir (src_path, pos)) ()
                     | SOME (digest, lines) => Exn.Res (blob_file src_path lines digest file_node)
                   end

--- a/src/Pure/Syntax/syntax_phases.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -215,7 +215,7 @@
         [ast] => ast
       | asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts));
 
-    val ast = Exn.interruptible_capture ast_of parsetree;
+    val ast = Exn.result ast_of parsetree;
   in (! reports, ast) end;
 
 
@@ -310,7 +310,7 @@
                 SOME (qs, (x, id)) => (report ps (markup_bound {def = false} qs) (x, id); t)
               | NONE => t);
 
-        val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
+        val tm' = Exn.result (fn () => decode [] [] [] tm) ();
       in (! reports, tm') end;
 
 end;
@@ -370,7 +370,7 @@
     val (ambig_msgs, asts) = parse_asts ctxt false root input;
     val results =
       (map o apsnd o Exn.maps_res)
-        (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts;
+        (Ast.normalize ctxt parse_rules #> Exn.result (ast_to_term ctxt tr)) asts;
   in (ambig_msgs, results) end;
 
 

--- a/src/Pure/Tools/build.scala	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Pure/Tools/build.scala	Mon Sep 25 18:45:41 2023 +0200
@@ -856,7 +856,7 @@
 
     val errors = new mutable.ListBuffer[String]
     for (session_name <- sessions) {
-      Exn.interruptible_capture(print(session_name)) match {
+      Exn.result(print(session_name)) match {
         case Exn.Res(_) =>
         case Exn.Exn(exn) => errors += Exn.message(exn)
       }

--- a/src/Tools/Code/code_runtime.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Tools/Code/code_runtime.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -99,7 +99,7 @@
     val (program_code, value_name) = comp vs_t;
     val value_code = space_implode " "
       (value_name :: "()" :: map (enclose "(" ")") args);
-  in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
+  in Exn.result (value ctxt cookie) (program_code, value_code) end;
 
 fun partiality_as_none e = SOME (Exn.release e)
   handle General.Match => NONE
@@ -390,7 +390,7 @@
 
 fun checked_computation cTs raw_computation ctxt =
   check_computation_input ctxt cTs
-  #> Exn.interruptible_capture raw_computation
+  #> Exn.result raw_computation
   #> partiality_as_none;
 
 fun mount_computation ctxt cTs T raw_computation lift_postproc =

--- a/src/Tools/quickcheck.ML	Mon Sep 25 17:37:52 2023 +0200
+++ b/src/Tools/quickcheck.ML	Mon Sep 25 18:45:41 2023 +0200
@@ -262,7 +262,7 @@
       try tester v
     else
       let (* FIXME !?!? *)
-        val tester = Exn.interruptible_capture tester v
+        val tester = Exn.result tester v
       in
         (case Exn.get_res tester of
           NONE => SOME (Exn.release tester)