src/Pure/Tools/debugger.scala
changeset 65344 b99283eed13c
parent 65223 844c067bc3d4
     1.1 --- a/src/Pure/Tools/debugger.scala	Sat Apr 01 19:16:19 2017 +0200
     1.2 +++ b/src/Pure/Tools/debugger.scala	Sat Apr 01 19:17:15 2017 +0200
     1.3 @@ -112,12 +112,11 @@
     1.4      {
     1.5        msg.properties match {
     1.6          case Markup.Debugger_State(thread_name) =>
     1.7 -          val msg_body =
     1.8 -            YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes)))
     1.9 +          val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes))
    1.10            val debug_states =
    1.11            {
    1.12              import XML.Decode._
    1.13 -            list(pair(properties, Symbol.decode_string))(msg_body).map({
    1.14 +            list(pair(properties, string))(msg_body).map({
    1.15                case (pos, function) => Debug_State(pos, function)
    1.16              })
    1.17            }
    1.18 @@ -131,7 +130,7 @@
    1.19      {
    1.20        msg.properties match {
    1.21          case Markup.Debugger_Output(thread_name) =>
    1.22 -          YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))) match {
    1.23 +          Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match {
    1.24              case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
    1.25                val message = XML.Elem(Markup(Markup.message(name), props), body)
    1.26                debugger.add_output(thread_name, i -> session.xml_cache.elem(message))