changeset 73557 | 225486d9c960 |
parent 73262 | 71b7a5775342 |
child 73558 | a5d1d1e2f109 |
--- a/src/Pure/System/message_channel.ML Sat Apr 10 21:50:59 2021 +0200 +++ b/src/Pure/System/message_channel.ML Sun Apr 11 21:23:51 2021 +0200 @@ -21,9 +21,7 @@ datatype message = Message of {body: XML.body, flush: bool}; -fun body_size body = fold (YXML.traverse (Integer.add o size)) body 0; - -fun chunk body = XML.Text (string_of_int (body_size body) ^ "\n") :: body; +fun chunk body = XML.Text (string_of_int (YXML.body_size body) ^ "\n") :: body; fun message name raw_props body = let