minor performance tuning: more direct YXML.bytes_of_body;
authorwenzelm
Thu, 27 Jun 2024 23:53:31 +0200
changeset 80436 6e865cd22349
parent 80435 de2ea807edd2
child 80437 2c07b9b2f9f4
minor performance tuning: more direct YXML.bytes_of_body;
src/Pure/Admin/build_log.scala
src/Pure/General/properties.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))
     }
 
--- 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)
     }
   }