src/Pure/Thy/sessions.scala
changeset 65592 f45609debe0d
parent 65580 66351f79c295
child 65593 607f7ad07a60
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Apr 27 11:19:22 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Apr 27 11:26:25 2017 +0200
     1.3 @@ -761,7 +761,7 @@
     1.4  
     1.5    def store(system_mode: Boolean = false): Store = new Store(system_mode)
     1.6  
     1.7 -  class Store private[Sessions](system_mode: Boolean)
     1.8 +  class Store private[Sessions](system_mode: Boolean) extends Properties.Store
     1.9    {
    1.10      /* file names */
    1.11  
    1.12 @@ -772,28 +772,6 @@
    1.13  
    1.14      /* SQL database content */
    1.15  
    1.16 -    val xml_cache: XML.Cache = new XML.Cache()
    1.17 -
    1.18 -    def encode_properties(ps: Properties.T): Bytes =
    1.19 -      Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
    1.20 -
    1.21 -    def decode_properties(bs: Bytes): Properties.T =
    1.22 -      xml_cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
    1.23 -
    1.24 -    def compress_properties(ps: List[Properties.T], options: XZ.Options = XZ.options()): Bytes =
    1.25 -    {
    1.26 -      if (ps.isEmpty) Bytes.empty
    1.27 -      else Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).compress(options)
    1.28 -    }
    1.29 -
    1.30 -    def uncompress_properties(bs: Bytes): List[Properties.T] =
    1.31 -    {
    1.32 -      if (bs.isEmpty) Nil
    1.33 -      else
    1.34 -        XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress().text)).
    1.35 -          map(xml_cache.props(_))
    1.36 -    }
    1.37 -
    1.38      def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
    1.39        using(Session_Info.select_statement(db, name, List(column)))(stmt =>
    1.40        {