author | wenzelm |
Mon, 10 Aug 2015 11:20:16 +0200 | |
changeset 60871 | 9b26f3118e40 |
parent 60870 | 6b7d10331b6b |
child 60872 | 9f45c2f1cbfd |
--- a/src/Pure/Tools/debugger.ML Sat Aug 08 22:08:43 2015 +0200 +++ b/src/Pure/Tools/debugger.ML Mon Aug 10 11:20:16 2015 +0200 @@ -152,6 +152,7 @@ val evaluate_verbose = evaluate {SML = SML, verbose = true}; val context1 = ML_Context.the_generic_context () |> Context_Position.set_visible_generic false + |> Config.put_generic ML_Options.debugger false |> ML_Env.add_name_space {SML = SML} (ML_Debugger.debug_name_space (the_debug_state thread_name index)); val context2 =