changeset 65344 | b99283eed13c |
parent 65220 | 420f55912b3e |
child 71601 | 97ccf48c2f0c |
--- a/src/Pure/Tools/print_operation.scala Sat Apr 01 19:16:19 2017 +0200 +++ b/src/Pure/Tools/print_operation.scala Sat Apr 01 19:17:15 2017 +0200 @@ -32,7 +32,7 @@ val ops = { import XML.Decode._ - list(pair(string, string))(YXML.parse_body(msg.text)) + list(pair(string, string))(Symbol.decode_yxml(msg.text)) } print_operations.change(_ => ops) true