| changeset 60871 | 9b26f3118e40 |
| parent 60869 | 878e32cf3131 |
| child 60878 | 1f0d2bbcf38b |
--- 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 =