--- a/src/Pure/Admin/build_stats.scala Fri May 05 18:15:53 2017 +0200
+++ b/src/Pure/Admin/build_stats.scala Fri May 05 18:32:18 2017 +0200
@@ -30,9 +30,8 @@
val all_infos =
Par_List.map((info: Jenkins.Job_Info) =>
{
- val t = info.timestamp / 1000
val log_file = Build_Log.Log_File(info.log_filename.implode, Url.read(info.main_log))
- (t, log_file.parse_build_info())
+ (info.date, log_file.parse_build_info())
}, job_infos)
val all_sessions =
(Set.empty[String] /: all_infos)(
@@ -55,11 +54,11 @@
Isabelle_System.with_tmp_file(session, "png") { data_file =>
Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file =>
val data =
- for { (t, info) <- all_infos if info.finished(session) }
+ for { (date, info) <- all_infos if info.finished(session) }
yield {
val timing1 = info.timing(session)
val timing2 = info.ml_timing(session)
- List(t.toString,
+ List(date.unix_epoch.toString,
timing1.elapsed.minutes,
timing1.cpu.minutes,
timing2.elapsed.minutes,
--- a/src/Pure/General/date.scala Fri May 05 18:15:53 2017 +0200
+++ b/src/Pure/General/date.scala Fri May 05 18:32:18 2017 +0200
@@ -93,6 +93,7 @@
def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
def to_utc: Date = to(ZoneId.of("UTC"))
+ def unix_epoch: Long = rep.toEpochSecond
def instant: Instant = Instant.from(rep)
def time: Time = Time.instant(instant)
def timezone: ZoneId = rep.getZone