# HG changeset patch
# User wenzelm
# Date 1618169031 -7200
# Node ID 225486d9c960c3e2d15e3b3bbed38cd3c5c2e4b3
# Parent  192bcee4f8b856e4f534bf218969fd8d1f48dfe4
tuned signature;

diff -r 192bcee4f8b8 -r 225486d9c960 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Apr 10 21:50:59 2021 +0200
+++ b/src/Pure/PIDE/yxml.ML	Sun Apr 11 21:23:51 2021 +0200
@@ -21,6 +21,8 @@
   val embed_controls: string -> string
   val detect: string -> bool
   val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
+  val tree_size: XML.tree -> int
+  val body_size: XML.body -> int
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
   val write_body: Path.T -> XML.body -> unit
@@ -63,7 +65,7 @@
 fun detect s = Char.contains s X_char orelse Char.contains s Y_char;
 
 
-(* output *)
+(* traverse *)
 
 fun traverse string =
   let
@@ -77,6 +79,12 @@
       | tree (XML.Text s) = string s;
   in tree end;
 
+fun tree_size tree = traverse (Integer.add o size) tree 0;
+fun body_size body = fold (Integer.add o tree_size) body 0;
+
+
+(* output *)
+
 fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
 val string_of = string_of_body o single;
 
diff -r 192bcee4f8b8 -r 225486d9c960 src/Pure/System/message_channel.ML
--- 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