# HG changeset patch
# User wenzelm
# Date 1697020631 -7200
# Node ID 6b3f13d396127f6069bb0393a89683e6123e5b8d
# Parent  6ca807f7fed02560754d4abb5756c3c0303933c8
proper Isabelle_Thread.try_catch;

diff -r 6ca807f7fed0 -r 6b3f13d39612 src/Pure/ML/ml_compiler0.ML
--- 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;