src/Pure/Tools/debugger.ML
changeset 62663 bea354f6ff21
parent 62516 5732f1c31566
child 62821 48c24d0b6d85
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
   187     val toks = ML_Lex.read_source SML (Input.string txt)
   187     val toks = ML_Lex.read_source SML (Input.string txt)
   188     val context = eval_context thread_name index SML toks;
   188     val context = eval_context thread_name index SML toks;
   189     val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);
   189     val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);
   190 
   190 
   191     fun print x =
   191     fun print x =
   192       Pretty.from_ML
   192       Pretty.from_polyml
   193         (ML_Pretty.from_polyml
   193         (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
   194           (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space)));
       
   195     fun print_all () =
   194     fun print_all () =
   196       #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
   195       #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
   197       |> sort_by #1 |> map (Pretty.item o single o print o #2)
   196       |> sort_by #1 |> map (Pretty.item o single o print o #2)
   198       |> Pretty.chunks |> Pretty.string_of |> writeln_message;
   197       |> Pretty.chunks |> Pretty.string_of |> writeln_message;
   199   in Context.setmp_thread_data (SOME context) print_all () end;
   198   in Context.setmp_thread_data (SOME context) print_all () end;