# HG changeset patch
# User wenzelm
# Date 1719525211 -7200
# Node ID 6e865cd2234982a49fe44e0566324b02502485ed
# Parent  de2ea807edd2fa30198e2f258efe7dc6c514de51
minor performance tuning: more direct YXML.bytes_of_body;

diff -r de2ea807edd2 -r 6e865cd22349 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu Jun 27 23:45:32 2024 +0200
+++ b/src/Pure/Admin/build_log.scala	Thu Jun 27 23:53:31 2024 +0200
@@ -650,7 +650,7 @@
   ): Option[Bytes] =
     if (errors.isEmpty) None
     else {
-      Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).
+      Some(YXML.bytes_of_body(XML.Encode.list(XML.Encode.string)(errors)).
         compress(cache = cache))
     }
 
diff -r de2ea807edd2 -r 6e865cd22349 src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Thu Jun 27 23:45:32 2024 +0200
+++ b/src/Pure/General/properties.scala	Thu Jun 27 23:53:31 2024 +0200
@@ -45,7 +45,7 @@
 
   def encode(ps: T): Bytes = {
     if (ps.isEmpty) Bytes.empty
-    else Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
+    else YXML.bytes_of_body(XML.Encode.properties(ps))
   }
 
   def decode(bs: Bytes, cache: XML.Cache = XML.Cache.none): T = {
@@ -59,7 +59,7 @@
   ): Bytes = {
     if (ps.isEmpty) Bytes.empty
     else {
-      Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).
+      YXML.bytes_of_body(XML.Encode.list(XML.Encode.properties)(ps)).
         compress(options = options, cache = cache)
     }
   }