diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Tools/debugger.ML --- a/src/Pure/Tools/debugger.ML Tue Sep 26 14:29:55 2023 +0200 +++ b/src/Pure/Tools/debugger.ML Tue Sep 26 14:42:33 2023 +0200 @@ -229,13 +229,13 @@ in fun debugger_loop thread_name = - Thread_Attributes.uninterruptible (fn run => fn () => + Thread_Attributes.uninterruptible_body (fn run => let fun loop () = (debugger_state thread_name; if debugger_command thread_name then loop () else ()); val result = Exn.capture (run with_debugging) loop; val _ = debugger_state thread_name; - in Exn.release result end) (); + in Exn.release result end); end;