# HG changeset patch
# User wenzelm
# Date 1493285185 -7200
# Node ID f45609debe0d8cd92c25ffa7d91c7dd3d42a08f7
# Parent  5953c7fbc2b823b689ceecba18d16d22a8f35caf
clarified modules;

diff -r 5953c7fbc2b8 -r f45609debe0d src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Thu Apr 27 11:19:22 2017 +0200
+++ b/src/Pure/General/properties.scala	Thu Apr 27 11:26:25 2017 +0200
@@ -79,5 +79,32 @@
         case Some((_, value)) => Value.Double.unapply(value)
       }
   }
+
+
+  /* cached store */
+
+  trait Store
+  {
+    val xml_cache: XML.Cache = new XML.Cache()
+
+    def encode_properties(ps: T): Bytes =
+      Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
+
+    def decode_properties(bs: Bytes): T =
+      xml_cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
+
+    def compress_properties(ps: List[T], options: XZ.Options = XZ.options()): Bytes =
+    {
+      if (ps.isEmpty) Bytes.empty
+      else Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).compress(options)
+    }
+
+    def uncompress_properties(bs: Bytes): List[T] =
+    {
+      if (bs.isEmpty) Nil
+      else
+        XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress().text)).
+          map(xml_cache.props(_))
+    }
+  }
 }
-
diff -r 5953c7fbc2b8 -r f45609debe0d src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Apr 27 11:19:22 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Apr 27 11:26:25 2017 +0200
@@ -761,7 +761,7 @@
 
   def store(system_mode: Boolean = false): Store = new Store(system_mode)
 
-  class Store private[Sessions](system_mode: Boolean)
+  class Store private[Sessions](system_mode: Boolean) extends Properties.Store
   {
     /* file names */
 
@@ -772,28 +772,6 @@
 
     /* SQL database content */
 
-    val xml_cache: XML.Cache = new XML.Cache()
-
-    def encode_properties(ps: Properties.T): Bytes =
-      Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
-
-    def decode_properties(bs: Bytes): Properties.T =
-      xml_cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
-
-    def compress_properties(ps: List[Properties.T], options: XZ.Options = XZ.options()): Bytes =
-    {
-      if (ps.isEmpty) Bytes.empty
-      else Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).compress(options)
-    }
-
-    def uncompress_properties(bs: Bytes): List[Properties.T] =
-    {
-      if (bs.isEmpty) Nil
-      else
-        XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress().text)).
-          map(xml_cache.props(_))
-    }
-
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
       using(Session_Info.select_statement(db, name, List(column)))(stmt =>
       {