more robust data representation: notably for Store.read_session_timing with database_server;
--- a/src/Pure/General/properties.scala Sun Aug 07 23:06:29 2022 +0200
+++ b/src/Pure/General/properties.scala Mon Aug 08 11:46:09 2022 +0200
@@ -43,10 +43,15 @@
/* external storage */
- def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
+ def encode(ps: T): Bytes = {
+ if (ps.isEmpty) Bytes.empty
+ else Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
+ }
- def decode(bs: Bytes, cache: XML.Cache = XML.Cache.none): T =
- cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
+ 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)))
+ }
def compress(ps: List[T],
options: XZ.Options = XZ.options(),