proper Isabelle_Thread.try_catch;

--- a/src/Pure/ML/ml_compiler0.ML	Wed Oct 11 12:22:46 2023 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Wed Oct 11 12:37:11 2023 +0200
@@ -106,13 +106,13 @@
       PolyML.Compiler.CPDebug debug] @
      (case print_depth of NONE => [] | SOME d => [PolyML.Compiler.CPPrintDepth (fn () => d)]);
     val _ =
-      (while not (List.null (! in_buffer)) do
-        PolyML.compiler (get, parameters) ())
-      handle exn =>
-        if Exn.is_interrupt exn then Exn.reraise exn
-        else
+      Isabelle_Thread.try_catch
+        (fn () =>
+          (while not (List.null (! in_buffer)) do
+            PolyML.compiler (get, parameters) ()))
+        (fn exn =>
          (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-          error (output ()); Exn.reraise exn);
+          error (output ()); Exn.reraise exn));
   in if verbose then print (output ()) else () end;
 
 end;