src/Pure/General/properties.scala
changeset 73031 f93f0597f4fb
parent 73024 337e1b135d2f
child 73712 3eba8d4b624b
--- a/src/Pure/General/properties.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/General/properties.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -37,8 +37,8 @@
 
   def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
 
-  def decode(bs: Bytes, xml_cache: XML.Cache = XML.Cache.none): T =
-    xml_cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
+  def decode(bs: Bytes, cache: XML.Cache = XML.Cache.none): T =
+    cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
 
   def compress(ps: List[T],
     options: XZ.Options = XZ.options(),
@@ -51,15 +51,14 @@
     }
   }
 
-  def uncompress(bs: Bytes,
-    cache: XZ.Cache = XZ.Cache(),
-    xml_cache: XML.Cache = XML.Cache.none): List[T] =
+  def uncompress(bs: Bytes, cache: XML.Cache = XML.Cache.none): List[T] =
   {
     if (bs.is_empty) Nil
     else {
       val ps =
-        XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text))
-      if (xml_cache.no_cache) ps else ps.map(xml_cache.props)
+        XML.Decode.list(XML.Decode.properties)(
+          YXML.parse_body(bs.uncompress(cache = cache.xz).text))
+      if (cache.no_cache) ps else ps.map(cache.props)
     }
   }