# HG changeset patch # User wenzelm # Date 1495049056 -7200 # Node ID 5d29d93766ef30f7a168457d3ebfccf07a5e5637 # Parent 69f4dacd31cfced41d6741025add0e7abfe33280 clarified use of XML.Cache; diff -r 69f4dacd31cf -r 5d29d93766ef src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Wed May 17 21:08:11 2017 +0200 +++ b/src/Pure/Admin/build_log.scala Wed May 17 21:24:16 2017 +0200 @@ -747,8 +747,10 @@ def store(options: Options): Store = new Store(options) - class Store private[Build_Log](options: Options) extends Properties.Store + class Store private[Build_Log](options: Options) { + val xml_cache: XML.Cache = new XML.Cache() + def open_database( user: String = options.string("build_log_database_user"), password: String = options.string("build_log_database_password"), @@ -889,7 +891,7 @@ { val ml_stats: List[(String, Option[Bytes])] = Par_List.map[(String, Session_Entry), (String, Option[Bytes])]( - { case (a, b) => (a, compress_properties(b.ml_statistics).proper) }, + { case (a, b) => (a, Properties.compress(b.ml_statistics).proper) }, build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList) val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None) for ((session_name, ml_statistics) <- entries) { @@ -1011,7 +1013,8 @@ heap_size = res.get_long(Data.heap_size), status = res.get_string(Data.status).map(Session_Status.withName(_)), ml_statistics = - if (ml_statistics) uncompress_properties(res.bytes(Data.ml_statistics)) + if (ml_statistics) + Properties.uncompress(res.bytes(Data.ml_statistics), Some(xml_cache)) else Nil) session_name -> session_entry }).toMap diff -r 69f4dacd31cf -r 5d29d93766ef src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Wed May 17 21:08:11 2017 +0200 +++ b/src/Pure/Admin/build_status.scala Wed May 17 21:24:16 2017 +0200 @@ -169,7 +169,7 @@ val ml_stats = ML_Statistics( if (ml_statistics) - store.uncompress_properties(res.bytes(Build_Log.Data.ml_statistics)) + Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics)) else Nil, heading = session_name + " (Isabelle/ " + isabelle_version + ")") val entry = diff -r 69f4dacd31cf -r 5d29d93766ef src/Pure/General/properties.scala --- a/src/Pure/General/properties.scala Wed May 17 21:08:11 2017 +0200 +++ b/src/Pure/General/properties.scala Wed May 17 21:24:16 2017 +0200 @@ -33,6 +33,38 @@ } + /* external storage */ + + def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(ps))) + + def decode(bs: Bytes, xml_cache: Option[XML.Cache] = None): T = + { + val ps = XML.Decode.properties(YXML.parse_body(bs.text)) + xml_cache match { + case None => ps + case Some(cache) => cache.props(ps) + } + } + + def compress(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(bs: Bytes, xml_cache: Option[XML.Cache] = None): List[T] = + { + if (bs.isEmpty) Nil + else { + val ps = XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress().text)) + xml_cache match { + case None => ps + case Some(cache) => ps.map(cache.props(_)) + } + } + } + + /* multi-line entries */ val separator = '\u000b' @@ -95,32 +127,4 @@ 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 69f4dacd31cf -r 5d29d93766ef src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed May 17 21:08:11 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Wed May 17 21:24:16 2017 +0200 @@ -750,7 +750,7 @@ def store(system_mode: Boolean = false): Store = new Store(system_mode) - class Store private[Sessions](system_mode: Boolean) extends Properties.Store + class Store private[Sessions](system_mode: Boolean) { /* file names */ @@ -761,6 +761,8 @@ /* SQL database content */ + val xml_cache = new XML.Cache() + def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes = db.using_statement(Session_Info.table.select(List(column), Session_Info.session_name.where_equal(name)))(stmt => @@ -770,7 +772,7 @@ }) def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] = - uncompress_properties(read_bytes(db, name, column)) + Properties.uncompress(read_bytes(db, name, column), Some(xml_cache)) /* output */ @@ -825,10 +827,10 @@ db.using_statement(Session_Info.table.insert())(stmt => { stmt.string(1) = name - stmt.bytes(2) = encode_properties(build_log.session_timing) - stmt.bytes(3) = compress_properties(build_log.command_timings) - stmt.bytes(4) = compress_properties(build_log.ml_statistics) - stmt.bytes(5) = compress_properties(build_log.task_statistics) + stmt.bytes(2) = Properties.encode(build_log.session_timing) + stmt.bytes(3) = Properties.compress(build_log.command_timings) + stmt.bytes(4) = Properties.compress(build_log.ml_statistics) + stmt.bytes(5) = Properties.compress(build_log.task_statistics) stmt.string(6) = cat_lines(build.sources) stmt.string(7) = cat_lines(build.input_heaps) stmt.string(8) = build.output_heap getOrElse "" @@ -839,7 +841,7 @@ } def read_session_timing(db: SQL.Database, name: String): Properties.T = - decode_properties(read_bytes(db, name, Session_Info.session_timing)) + Properties.decode(read_bytes(db, name, Session_Info.session_timing), Some(xml_cache)) def read_command_timings(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.command_timings)