# HG changeset patch
# User wenzelm
# Date 1493455052 -7200
# Node ID e6c0afe672fa7714830cf3526c9a9c231b0c0fb9
# Parent  fd87fb909b892ed79909897f8c9ff30bdaeb4582
optional ml_statistics: much faster;

diff -r fd87fb909b89 -r e6c0afe672fa src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Apr 29 10:33:43 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Sat Apr 29 10:37:32 2017 +0200
@@ -763,8 +763,15 @@
     }
 
     def read_build_info(
-      db: SQL.Database, log_name: String, session_names: List[String] = Nil): Build_Info =
+      db: SQL.Database,
+      log_name: String,
+      session_names: List[String] = Nil,
+      ml_statistics: Boolean = false): Build_Info =
     {
+      val columns =
+        Build_Info.table.columns.filter(c =>
+          c != Meta_Info.log_name && (ml_statistics || c != Build_Info.ml_statistics))
+
       val where0 =
         Meta_Info.log_name.sql_where_equal(log_name) + " AND " +
           Build_Info.session_name.sql_name + " <> ''"
@@ -774,8 +781,9 @@
           where0 + " AND " +
           session_names.map(a => Build_Info.session_name.sql_name + " = " + SQL.quote_string(a)).
             mkString("(", " OR ", ")")
+
       val sessions =
-        using(db.select(Build_Info.table, Build_Info.table.columns.tail, where))(stmt =>
+        using(db.select(Build_Info.table, columns, where))(stmt =>
         {
           SQL.iterator(stmt.executeQuery)(rs =>
           {
@@ -795,7 +803,9 @@
                     Time.ms(db.long(rs, Build_Info.ml_timing_gc))),
                 heap_size = db.get(rs, Build_Info.heap_size, db.long _),
                 status = Session_Status.withName(db.string(rs, Build_Info.status)),
-                ml_statistics = uncompress_properties(db.bytes(rs, Build_Info.ml_statistics)))
+                ml_statistics =
+                  if (ml_statistics) uncompress_properties(db.bytes(rs, Build_Info.ml_statistics))
+                  else Nil)
             session_name -> session_entry
           }).toMap
         })