# HG changeset patch # User wenzelm # Date 1695660341 -7200 # Node ID fde0b195cb7d3386e0b66abc25e516987076b4b7 # Parent b54aee45cabe3a3bf10e19ef6cf2db080c4e4aad clarified signature: avoid association with potentially dangerous Exn.capture; diff -r b54aee45cabe -r fde0b195cb7d src/Doc/Implementation/ML.thy --- 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>\Exn.interruptible_capture\ is similar to \<^ML>\Exn.capture\, but - interrupts are immediately re-raised as required for user code. + \<^descr> \<^ML>\Exn.result\ is similar to \<^ML>\Exn.capture\, but interrupts are + immediately re-raised as required for user code. \<^descr> \<^ML>\Exn.release\~\result\ releases the original runtime result, exposing its regular value or raising the reified exception. diff -r b54aee45cabe -r fde0b195cb7d src/HOL/Library/code_test.ML --- 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 diff -r b54aee45cabe -r fde0b195cb7d src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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 diff -r b54aee45cabe -r fde0b195cb7d src/Pure/Concurrent/future.ML --- 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; diff -r b54aee45cabe -r fde0b195cb7d src/Pure/Concurrent/par_list.ML --- 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 diff -r b54aee45cabe -r fde0b195cb7d src/Pure/General/exn.ML --- 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; diff -r b54aee45cabe -r fde0b195cb7d src/Pure/General/exn.scala --- 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) } diff -r b54aee45cabe -r fde0b195cb7d src/Pure/General/timing.ML --- 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; diff -r b54aee45cabe -r fde0b195cb7d src/Pure/Isar/proof.ML --- 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) diff -r b54aee45cabe -r fde0b195cb7d src/Pure/ML/exn_debugger.ML --- 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 diff -r b54aee45cabe -r fde0b195cb7d src/Pure/PIDE/command.ML --- 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 diff -r b54aee45cabe -r fde0b195cb7d src/Pure/Syntax/syntax_phases.ML --- 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; diff -r b54aee45cabe -r fde0b195cb7d src/Pure/Tools/build.scala --- 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) } diff -r b54aee45cabe -r fde0b195cb7d src/Tools/Code/code_runtime.ML --- 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 = diff -r b54aee45cabe -r fde0b195cb7d src/Tools/quickcheck.ML --- 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)