src/Pure/Tools/debugger.scala
changeset 65344 b99283eed13c
parent 65223 844c067bc3d4
child 71601 97ccf48c2f0c
equal deleted inserted replaced
65343:0a8e30a7b10e 65344:b99283eed13c
   110 
   110 
   111     private def debugger_state(msg: Prover.Protocol_Output): Boolean =
   111     private def debugger_state(msg: Prover.Protocol_Output): Boolean =
   112     {
   112     {
   113       msg.properties match {
   113       msg.properties match {
   114         case Markup.Debugger_State(thread_name) =>
   114         case Markup.Debugger_State(thread_name) =>
   115           val msg_body =
   115           val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes))
   116             YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes)))
       
   117           val debug_states =
   116           val debug_states =
   118           {
   117           {
   119             import XML.Decode._
   118             import XML.Decode._
   120             list(pair(properties, Symbol.decode_string))(msg_body).map({
   119             list(pair(properties, string))(msg_body).map({
   121               case (pos, function) => Debug_State(pos, function)
   120               case (pos, function) => Debug_State(pos, function)
   122             })
   121             })
   123           }
   122           }
   124           debugger.update_thread(thread_name, debug_states)
   123           debugger.update_thread(thread_name, debug_states)
   125           true
   124           true
   129 
   128 
   130     private def debugger_output(msg: Prover.Protocol_Output): Boolean =
   129     private def debugger_output(msg: Prover.Protocol_Output): Boolean =
   131     {
   130     {
   132       msg.properties match {
   131       msg.properties match {
   133         case Markup.Debugger_Output(thread_name) =>
   132         case Markup.Debugger_Output(thread_name) =>
   134           YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))) match {
   133           Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match {
   135             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
   134             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
   136               val message = XML.Elem(Markup(Markup.message(name), props), body)
   135               val message = XML.Elem(Markup(Markup.message(name), props), body)
   137               debugger.add_output(thread_name, i -> session.xml_cache.elem(message))
   136               debugger.add_output(thread_name, i -> session.xml_cache.elem(message))
   138               true
   137               true
   139             case _ => false
   138             case _ => false