src/Pure/Tools/debugger.ML

   map ML_Lex.read
    ["Context.put_generic_context (SOME (Context.Theory ML_context))",
     "Context.put_generic_context (SOME (Context.Proof ML_context))",
     "Context.put_generic_context (SOME ML_context)"];
 
-fun make_environment sml = if sml then ML_Env.SML else ML_Env.Isabelle;
+fun environment SML = if SML then ML_Env.SML else ML_Env.Isabelle;
+fun operations SML = if SML then ML_Env.SML_operations else ML_Env.Isabelle_operations;
 
 fun evaluate {SML, verbose} =
   ML_Context.eval
-    {environment = make_environment SML, redirect = false, verbose = verbose,
+    {environment = environment SML, redirect = false, verbose = verbose,
       debug = SOME false, writeln = writeln_message, warning = warning_message}
     Position.none;
 
 fun eval_setup thread_name index SML context =
   context
   |> Context_Position.set_visible_generic false
-  |> ML_Env.add_name_space (make_environment SML)
+  |> ML_Env.add_name_space (environment SML)
       (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index));
 
 fun eval_context thread_name index SML toks =
   let
     val context = Context.the_generic_context ();

 
 in
 
 fun eval thread_name index SML txt1 txt2 =
   let
-    val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
+    val (toks1, toks2) = apply2 (#read_source (operations SML) o Input.string) (txt1, txt2);
     val context = eval_context thread_name index SML toks1;
   in Context.setmp_generic_context (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
 
 fun print_vals thread_name index SML txt =
   let
-    val toks = ML_Lex.read_source SML (Input.string txt)
+    val toks = #read_source (operations SML) (Input.string txt)
     val context = eval_context thread_name index SML toks;
     val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index);
 
     fun print x =
       Pretty.from_polyml