src/Pure/Tools/debugger.ML
changeset 60904 e0fab97c989f
parent 60897 7aad4be8a48e
child 60924 610794dff23c
equal deleted inserted replaced
60903:bca464396b80 60904:e0fab97c989f
   163 
   163 
   164 fun eval thread_name index SML txt1 txt2 =
   164 fun eval thread_name index SML txt1 txt2 =
   165   let
   165   let
   166     val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
   166     val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
   167     val context = eval_context thread_name index SML toks1;
   167     val context = eval_context thread_name index SML toks1;
   168   in Context.setmp_thread_data (SOME context) evaluate {SML = SML, verbose = true} toks2 end;
   168   in Context.setmp_thread_data (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
   169 
   169 
   170 fun print_vals thread_name index SML txt =
   170 fun print_vals thread_name index SML txt =
   171   let
   171   let
   172     val context = eval_context thread_name index SML (ML_Lex.read_source SML (Input.string txt));
   172     val context = eval_context thread_name index SML (ML_Lex.read_source SML (Input.string txt));
   173     val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);
   173     val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);