--- a/src/Pure/Admin/build_history.scala Fri May 26 15:19:21 2017 +0200
+++ b/src/Pure/Admin/build_history.scala Fri May 26 15:28:46 2017 +0200
@@ -241,7 +241,7 @@
val properties =
if (database.is_file) {
using(SQLite.open_database(database))(db =>
- store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
+ store.read_ml_statistics(db, session_name))
}
else if (log_gz.is_file) {
Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
--- a/src/Pure/Admin/jenkins.scala Fri May 26 15:19:21 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala Fri May 26 15:28:46 2017 +0200
@@ -84,8 +84,7 @@
case Some(url) =>
Isabelle_System.with_tmp_file(session_name, "db") { database =>
Bytes.write(database, Bytes.read(url))
- using(SQLite.open_database(database))(db =>
- store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
+ using(SQLite.open_database(database))(db => store.read_ml_statistics(db, session_name))
}
case None =>
get_log("gz") match {
--- a/src/Pure/Tools/build.scala Fri May 26 15:19:21 2017 +0200
+++ b/src/Pure/Tools/build.scala Fri May 26 15:28:46 2017 +0200
@@ -51,9 +51,13 @@
try {
using(SQLite.open_database(database))(db =>
{
- val build_log = store.read_build_log(db, name, command_timings = true)
- val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
- (build_log.command_timings, session_timing)
+ val command_timings = store.read_command_timings(db, name)
+ val session_timing =
+ store.read_session_timing(db, name) match {
+ case Markup.Elapsed(t) => t
+ case _ => 0.0
+ }
+ (command_timings, session_timing)
})
}
catch {