--- 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
--- 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 =
--- 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(_))
- }
- }
}
--- 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)