clarified ML options;
authorwenzelm
Mon, 10 Aug 2015 11:20:16 +0200
changeset 60871 9b26f3118e40
parent 60870 6b7d10331b6b
child 60872 9f45c2f1cbfd
clarified ML options;
src/Pure/Tools/debugger.ML
--- 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 =