# HG changeset patch
# User wenzelm
# Date 1493728848 -7200
# Node ID 70b0ef74ef3a68debc4e643c63e4525ead7feebb
# Parent  3722be87305c507878fd50fccd130452459d9418
some derived data fields, to facilitate queries;

diff -r 3722be87305c -r 70b0ef74ef3a src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue May 02 14:27:59 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue May 02 14:40:48 2017 +0200
@@ -480,9 +480,11 @@
     val timing_elapsed = SQL.Column.long("timing_elapsed")
     val timing_cpu = SQL.Column.long("timing_cpu")
     val timing_gc = SQL.Column.long("timing_gc")
+    val timing_factor = SQL.Column.double("timing_factor")
     val ml_timing_elapsed = SQL.Column.long("ml_timing_elapsed")
     val ml_timing_cpu = SQL.Column.long("ml_timing_cpu")
     val ml_timing_gc = SQL.Column.long("ml_timing_gc")
+    val ml_timing_factor = SQL.Column.double("ml_timing_factor")
     val heap_size = SQL.Column.long("heap_size")
     val status = SQL.Column.string("status")
     val ml_statistics = SQL.Column.bytes("ml_statistics")
@@ -490,7 +492,8 @@
     val sessions_table =
       SQL.Table("isabelle_build_log_sessions",
         List(Meta_Info.log_name, session_name, chapter, groups, threads, timing_elapsed, timing_cpu,
-          timing_gc, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, heap_size, status))
+          timing_gc, timing_factor, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, ml_timing_factor,
+          heap_size, status))
     val ml_statistics_table =
       SQL.Table("isabelle_build_log_ml_statistics",
         List(Meta_Info.log_name, session_name, ml_statistics))
@@ -720,11 +723,13 @@
             db.set_long(stmt, 6, session.timing.elapsed.proper_ms)
             db.set_long(stmt, 7, session.timing.cpu.proper_ms)
             db.set_long(stmt, 8, session.timing.gc.proper_ms)
-            db.set_long(stmt, 9, session.ml_timing.elapsed.proper_ms)
-            db.set_long(stmt, 10, session.ml_timing.cpu.proper_ms)
-            db.set_long(stmt, 11, session.ml_timing.gc.proper_ms)
-            db.set_long(stmt, 12, session.heap_size)
-            db.set_string(stmt, 13, session.status.map(_.toString))
+            db.set_double(stmt, 9, session.timing.factor)
+            db.set_long(stmt, 10, session.ml_timing.elapsed.proper_ms)
+            db.set_long(stmt, 11, session.ml_timing.cpu.proper_ms)
+            db.set_long(stmt, 12, session.ml_timing.gc.proper_ms)
+            db.set_double(stmt, 13, session.ml_timing.factor)
+            db.set_long(stmt, 14, session.heap_size)
+            db.set_string(stmt, 15, session.status.map(_.toString))
             stmt.execute()
           }
         })