--- a/src/Pure/Tools/debugger.ML Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/Tools/debugger.ML Thu Sep 28 14:43:07 2023 +0200
@@ -29,10 +29,10 @@
val warning_message = output_message Markup.warningN;
val error_message = output_message Markup.errorN;
-fun error_wrapper e = e ()
- handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn
- else error_message (Runtime.exn_message exn);
+fun error_wrapper e =
+ (case Exn.result e () of
+ Exn.Res res => res
+ | Exn.Exn exn => error_message (Runtime.exn_message exn));
(* thread input *)