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;