equal
deleted
inserted
replaced
207 |
207 |
208 fun debugger_state thread_name = |
208 fun debugger_state thread_name = |
209 Output.protocol_message (Markup.debugger_state thread_name) |
209 Output.protocol_message (Markup.debugger_state thread_name) |
210 [get_debugging () |
210 [get_debugging () |
211 |> map (fn st => |
211 |> map (fn st => |
212 (Position.properties_of (Exn_Properties.position_of_location (ML_Debugger.debug_location st)), |
212 (Position.properties_of |
|
213 (Exn_Properties.position_of_polyml_location (ML_Debugger.debug_location st)), |
213 ML_Debugger.debug_function st)) |
214 ML_Debugger.debug_function st)) |
214 |> let open XML.Encode in list (pair properties string) end |
215 |> let open XML.Encode in list (pair properties string) end |
215 |> YXML.string_of_body]; |
216 |> YXML.string_of_body]; |
216 |
217 |
217 fun debugger_command thread_name = |
218 fun debugger_command thread_name = |