src/Pure/Tools/debugger.ML
changeset 62516 5732f1c31566
parent 62505 9e2a65912111
child 62663 bea354f6ff21
equal deleted inserted replaced
62515:e73644de5db8 62516:5732f1c31566
   208 
   208 
   209 fun debugger_state thread_name =
   209 fun debugger_state thread_name =
   210   Output.protocol_message (Markup.debugger_state thread_name)
   210   Output.protocol_message (Markup.debugger_state thread_name)
   211    [get_debugging ()
   211    [get_debugging ()
   212     |> map (fn st =>
   212     |> map (fn st =>
   213       (Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)),
   213       (Position.properties_of (Exn_Properties.position_of_location (ML_Debugger.debug_location st)),
   214        ML_Debugger.debug_function st))
   214        ML_Debugger.debug_function st))
   215     |> let open XML.Encode in list (pair properties string) end
   215     |> let open XML.Encode in list (pair properties string) end
   216     |> YXML.string_of_body];
   216     |> YXML.string_of_body];
   217 
   217 
   218 fun debugger_command thread_name =
   218 fun debugger_command thread_name =