Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sat, 06 May 2017 12:52:29 +0200
changeset 65741 cf42659364c9
parent 65740 83388f09e9ab
child 65742 b9e0f25ba16a
tuned;
src/Pure/Admin/build_log.scala file | annotate | diff | comparison | revisions
src/Pure/Admin/build_stats.scala file | annotate | diff | comparison | revisions
src/Pure/General/sql.scala file | annotate | diff | comparison | revisions 
--- 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 =
--- 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)
--- 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)
isabelle