# HG changeset patch
# User wenzelm
# Date 1659951969 -7200
# Node ID 1c3c313199746c1e9743ede72fd162e6d5f484d9
# Parent  5e00c5ffc040fc83d62acb79d29ac9727c36cce0
more robust data representation: notably for Store.read_session_timing with database_server;

diff -r 5e00c5ffc040 -r 1c3c31319974 src/Pure/General/properties.scala
--- 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(),