src/Pure/Tools/print_operation.scala
changeset 65344 b99283eed13c
parent 65220 420f55912b3e
child 71601 97ccf48c2f0c
equal deleted inserted replaced
65343:0a8e30a7b10e 65344:b99283eed13c
    30     private def put(msg: Prover.Protocol_Output): Boolean =
    30     private def put(msg: Prover.Protocol_Output): Boolean =
    31     {
    31     {
    32       val ops =
    32       val ops =
    33       {
    33       {
    34         import XML.Decode._
    34         import XML.Decode._
    35         list(pair(string, string))(YXML.parse_body(msg.text))
    35         list(pair(string, string))(Symbol.decode_yxml(msg.text))
    36       }
    36       }
    37       print_operations.change(_ => ops)
    37       print_operations.change(_ => ops)
    38       true
    38       true
    39     }
    39     }
    40 
    40