src/Pure/Thy/sessions.scala
changeset 65857 5d29d93766ef
parent 65833 95fd3b9888e6
child 65934 5f202ba9f590
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed May 17 21:08:11 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed May 17 21:24:16 2017 +0200
     1.3 @@ -750,7 +750,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) extends Properties.Store
     1.8 +  class Store private[Sessions](system_mode: Boolean)
     1.9    {
    1.10      /* file names */
    1.11  
    1.12 @@ -761,6 +761,8 @@
    1.13  
    1.14      /* SQL database content */
    1.15  
    1.16 +    val xml_cache = new XML.Cache()
    1.17 +
    1.18      def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
    1.19        db.using_statement(Session_Info.table.select(List(column),
    1.20          Session_Info.session_name.where_equal(name)))(stmt =>
    1.21 @@ -770,7 +772,7 @@
    1.22        })
    1.23  
    1.24      def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
    1.25 -      uncompress_properties(read_bytes(db, name, column))
    1.26 +      Properties.uncompress(read_bytes(db, name, column), Some(xml_cache))
    1.27  
    1.28  
    1.29      /* output */
    1.30 @@ -825,10 +827,10 @@
    1.31          db.using_statement(Session_Info.table.insert())(stmt =>
    1.32          {
    1.33            stmt.string(1) = name
    1.34 -          stmt.bytes(2) = encode_properties(build_log.session_timing)
    1.35 -          stmt.bytes(3) = compress_properties(build_log.command_timings)
    1.36 -          stmt.bytes(4) = compress_properties(build_log.ml_statistics)
    1.37 -          stmt.bytes(5) = compress_properties(build_log.task_statistics)
    1.38 +          stmt.bytes(2) = Properties.encode(build_log.session_timing)
    1.39 +          stmt.bytes(3) = Properties.compress(build_log.command_timings)
    1.40 +          stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
    1.41 +          stmt.bytes(5) = Properties.compress(build_log.task_statistics)
    1.42            stmt.string(6) = cat_lines(build.sources)
    1.43            stmt.string(7) = cat_lines(build.input_heaps)
    1.44            stmt.string(8) = build.output_heap getOrElse ""
    1.45 @@ -839,7 +841,7 @@
    1.46      }
    1.47  
    1.48      def read_session_timing(db: SQL.Database, name: String): Properties.T =
    1.49 -      decode_properties(read_bytes(db, name, Session_Info.session_timing))
    1.50 +      Properties.decode(read_bytes(db, name, Session_Info.session_timing), Some(xml_cache))
    1.51  
    1.52      def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
    1.53        read_properties(db, name, Session_Info.command_timings)