src/Pure/General/properties.scala
changeset 73024 337e1b135d2f
parent 72885 1b0f81e556a2
child 73031 f93f0597f4fb
equal deleted inserted replaced
73023:e15621aa8c72 73024:337e1b135d2f
    35 
    35 
    36   /* external storage */
    36   /* external storage */
    37 
    37 
    38   def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
    38   def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
    39 
    39 
    40   def decode(bs: Bytes, xml_cache: Option[XML.Cache] = None): T =
    40   def decode(bs: Bytes, xml_cache: XML.Cache = XML.Cache.none): T =
    41   {
    41     xml_cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
    42     val ps = XML.Decode.properties(YXML.parse_body(bs.text))
       
    43     xml_cache match {
       
    44       case None => ps
       
    45       case Some(cache) => cache.props(ps)
       
    46     }
       
    47   }
       
    48 
    42 
    49   def compress(ps: List[T],
    43   def compress(ps: List[T],
    50     options: XZ.Options = XZ.options(),
    44     options: XZ.Options = XZ.options(),
    51     cache: XZ.Cache = XZ.cache()): Bytes =
    45     cache: XZ.Cache = XZ.Cache()): Bytes =
    52   {
    46   {
    53     if (ps.isEmpty) Bytes.empty
    47     if (ps.isEmpty) Bytes.empty
    54     else {
    48     else {
    55       Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).
    49       Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).
    56         compress(options = options, cache = cache)
    50         compress(options = options, cache = cache)
    57     }
    51     }
    58   }
    52   }
    59 
    53 
    60   def uncompress(bs: Bytes,
    54   def uncompress(bs: Bytes,
    61     cache: XZ.Cache = XZ.cache(),
    55     cache: XZ.Cache = XZ.Cache(),
    62     xml_cache: Option[XML.Cache] = None): List[T] =
    56     xml_cache: XML.Cache = XML.Cache.none): List[T] =
    63   {
    57   {
    64     if (bs.is_empty) Nil
    58     if (bs.is_empty) Nil
    65     else {
    59     else {
    66       val ps =
    60       val ps =
    67         XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text))
    61         XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text))
    68       xml_cache match {
    62       if (xml_cache.no_cache) ps else ps.map(xml_cache.props)
    69         case None => ps
       
    70         case Some(cache) => ps.map(cache.props)
       
    71       }
       
    72     }
    63     }
    73   }
    64   }
    74 
    65 
    75 
    66 
    76   /* multi-line entries */
    67   /* multi-line entries */