src/Pure/Tools/debugger.ML
changeset 78728 72631efa3821
parent 78725 3c02ad5a1586
child 80809 4a64fc4d1cde
--- a/src/Pure/Tools/debugger.ML	Thu Sep 28 19:40:20 2023 +0200
+++ b/src/Pure/Tools/debugger.ML	Thu Sep 28 20:07:30 2023 +0200
@@ -137,7 +137,7 @@
 
 fun evaluate {SML, verbose} =
   ML_Context.eval
-    {environment = environment SML, redirect = false, verbose = verbose,
+    {environment = environment SML, redirect = false, verbose = verbose, catch_all = SML,
       debug = SOME false, writeln = writeln_message, warning = warning_message}
     Position.none;