src/Pure/General/properties.scala
changeset 80480 972f7a4cdc0e
parent 80436 6e865cd22349
child 80505 e3af424fdd1a
--- a/src/Pure/General/properties.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/General/properties.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -50,7 +50,7 @@
 
   def decode(bs: Bytes, cache: XML.Cache = XML.Cache.none): T = {
     if (bs.is_empty) Nil
-    else cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
+    else cache.props(XML.Decode.properties(YXML.parse_body(bs)))
   }
 
   def compress(ps: List[T],
@@ -69,7 +69,7 @@
     else {
       val ps =
         XML.Decode.list(XML.Decode.properties)(
-          YXML.parse_body(bs.uncompress(cache = cache.compress).text))
+          YXML.parse_body(bs.uncompress(cache = cache.compress)))
       if (cache.no_cache) ps else ps.map(cache.props)
     }
   }