# HG changeset patch
# User wenzelm
# Date 1494067949 -7200
# Node ID cf42659364c9ed2c8da5b6eebc4c0aa8bb958517
# Parent  83388f09e9ab3bcd78d1c7f7fc6e8fea98efcc98
tuned;

diff -r 83388f09e9ab -r cf42659364c9 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat May 06 12:45:42 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Sat May 06 12:52:29 2017 +0200
@@ -994,16 +994,9 @@
                 chapter = res.string(Data.chapter),
                 groups = split_lines(res.string(Data.groups)),
                 threads = res.get_int(Data.threads),
-                timing =
-                  Timing(
-                    Time.ms(res.long(Data.timing_elapsed)),
-                    Time.ms(res.long(Data.timing_cpu)),
-                    Time.ms(res.long(Data.timing_gc))),
+                timing = res.timing(Data.timing_elapsed, Data.timing_cpu, Data.timing_gc),
                 ml_timing =
-                  Timing(
-                    Time.ms(res.long(Data.ml_timing_elapsed)),
-                    Time.ms(res.long(Data.ml_timing_cpu)),
-                    Time.ms(res.long(Data.ml_timing_gc))),
+                  res.timing(Data.ml_timing_elapsed, Data.ml_timing_cpu, Data.ml_timing_gc),
                 heap_size = res.get_long(Data.heap_size),
                 status = res.get_string(Data.status).map(Session_Status.withName(_)),
                 ml_statistics =
diff -r 83388f09e9ab -r cf42659364c9 src/Pure/Admin/build_stats.scala
--- a/src/Pure/Admin/build_stats.scala	Sat May 06 12:45:42 2017 +0200
+++ b/src/Pure/Admin/build_stats.scala	Sat May 06 12:52:29 2017 +0200
@@ -91,14 +91,14 @@
             val session = res.string(Build_Log.Data.session_name)
             val entry =
               Entry(res.date(Build_Log.Data.pull_date),
-                Timing(
-                  Time.ms(res.long(Build_Log.Data.timing_elapsed)),
-                  Time.ms(res.long(Build_Log.Data.timing_cpu)),
-                  Time.ms(res.long(Build_Log.Data.timing_gc))),
-                Timing(
-                  Time.ms(res.long(Build_Log.Data.ml_timing_elapsed)),
-                  Time.ms(res.long(Build_Log.Data.ml_timing_cpu)),
-                  Time.ms(res.long(Build_Log.Data.ml_timing_gc))))
+                res.timing(
+                  Build_Log.Data.timing_elapsed,
+                  Build_Log.Data.timing_cpu,
+                  Build_Log.Data.timing_gc),
+                res.timing(
+                  Build_Log.Data.ml_timing_elapsed,
+                  Build_Log.Data.ml_timing_cpu,
+                  Build_Log.Data.ml_timing_gc))
 
             val session_entries = data.getOrElse(name, Map.empty)
             val entries = session_entries.getOrElse(session, Nil)
diff -r 83388f09e9ab -r cf42659364c9 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sat May 06 12:45:42 2017 +0200
+++ b/src/Pure/General/sql.scala	Sat May 06 12:52:29 2017 +0200
@@ -254,6 +254,9 @@
     }
     def date(column: Column): Date = stmt.db.date(res, column)
 
+    def timing(c1: Column, c2: Column, c3: Column) =
+      Timing(Time.ms(long(c1)), Time.ms(long(c2)), Time.ms(long(c3)))
+
     def get[A](column: Column, f: Column => A): Option[A] =
     {
       val x = f(column)