src/Tools/Code/code_runtime.ML
changeset 78705 fde0b195cb7d
parent 77889 5db014c36f42
child 78795 f7e972d567f3
--- 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 =