--- a/src/Pure/Admin/build_log.scala Sat Apr 29 10:06:16 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Sat Apr 29 10:17:08 2017 +0200
@@ -439,9 +439,9 @@
threads: Option[Int],
timing: Timing,
ml_timing: Timing,
- ml_statistics: List[Properties.T],
heap_size: Option[Long],
- status: Session_Status.Value)
+ status: Session_Status.Value,
+ ml_statistics: List[Properties.T])
{
def finished: Boolean = status == Session_Status.FINISHED
}
@@ -458,13 +458,13 @@
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_statistics = SQL.Column.bytes("ml_statistics")
val heap_size = SQL.Column.long("heap_size")
val status = SQL.Column.string("status")
+ val ml_statistics = SQL.Column.bytes("ml_statistics")
val table = SQL.Table("isabelle_build_log_build_info",
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, ml_statistics, heap_size, status))
+ timing_gc, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, heap_size, status, ml_statistics))
val table0 = table.copy(columns = table.columns.take(2))
}
@@ -520,12 +520,12 @@
var started = Set.empty[String]
var failed = Set.empty[String]
var cancelled = Set.empty[String]
+ var heap_sizes = Map.empty[String, Long]
var ml_statistics = Map.empty[String, List[Properties.T]]
- var heap_sizes = Map.empty[String, Long]
def all_sessions: Set[String] =
chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
- failed ++ cancelled ++ started ++ ml_statistics.keySet ++ heap_sizes.keySet
+ failed ++ cancelled ++ started ++ heap_sizes.keySet ++ ml_statistics.keySet
for (line <- log_file.lines) {
@@ -593,9 +593,9 @@
threads.get(name),
timing.getOrElse(name, Timing.zero),
ml_timing.getOrElse(name, Timing.zero),
- ml_statistics.getOrElse(name, Nil).reverse,
heap_sizes.get(name),
- status)
+ status,
+ ml_statistics.getOrElse(name, Nil).reverse)
(name -> entry)
}):_*)
Build_Info(sessions)
@@ -750,9 +750,9 @@
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_bytes(stmt, 12, compress_properties(session.ml_statistics))
- db.set_long(stmt, 13, session.heap_size)
- db.set_string(stmt, 14, session.status.toString)
+ db.set_long(stmt, 12, session.heap_size)
+ db.set_string(stmt, 13, session.status.toString)
+ db.set_bytes(stmt, 14, compress_properties(session.ml_statistics))
stmt.execute()
}
})
@@ -793,9 +793,9 @@
Timing(Time.ms(db.long(rs, Build_Info.ml_timing_elapsed)),
Time.ms(db.long(rs, Build_Info.ml_timing_cpu)),
Time.ms(db.long(rs, Build_Info.ml_timing_gc))),
- ml_statistics = uncompress_properties(db.bytes(rs, Build_Info.ml_statistics)),
heap_size = db.get(rs, Build_Info.heap_size, db.long _),
- status = Session_Status.withName(db.string(rs, Build_Info.status)))
+ status = Session_Status.withName(db.string(rs, Build_Info.status)),
+ ml_statistics = uncompress_properties(db.bytes(rs, Build_Info.ml_statistics)))
session_name -> session_entry
}).toMap
})