--- 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)
}
}