# HG changeset patch
# User wenzelm
# Date 1495805326 -7200
# Node ID 73c099fa96a4e4a86a572b771dde198c07c7f54d
# Parent  5f202ba9f590990c853143ae33b9028f67f555bd
more selective database access;

diff -r 5f202ba9f590 -r 73c099fa96a4 src/Pure/Admin/build_history.scala
--- 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
diff -r 5f202ba9f590 -r 73c099fa96a4 src/Pure/Admin/jenkins.scala
--- 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 {
diff -r 5f202ba9f590 -r 73c099fa96a4 src/Pure/Tools/build.scala
--- 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 {