--- a/src/Pure/Admin/build_history.scala Sat Mar 18 22:11:05 2017 +0100
+++ b/src/Pure/Admin/build_history.scala Sun Mar 19 11:56:56 2017 +0100
@@ -230,11 +230,10 @@
val properties =
if (database.is_file) {
using(SQLite.open_database(database))(db =>
- store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
+ store.read_build_log(db, ml_statistics = true)).ml_statistics
}
else if (log_gz.is_file) {
- Build_Log.Log_File(log_gz).
- parse_session_info(session_name, ml_statistics = true).ml_statistics
+ Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
}
else Nil
properties.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
--- a/src/Pure/Admin/build_log.scala Sat Mar 18 22:11:05 2017 +0100
+++ b/src/Pure/Admin/build_log.scala Sun Mar 19 11:56:56 2017 +0100
@@ -255,12 +255,10 @@
def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
def parse_session_info(
- default_name: String = "",
command_timings: Boolean = false,
ml_statistics: Boolean = false,
task_statistics: Boolean = false): Session_Info =
- Build_Log.parse_session_info(
- log_file, default_name, command_timings, ml_statistics, task_statistics)
+ Build_Log.parse_session_info(log_file, command_timings, ml_statistics, task_statistics)
}
@@ -542,7 +540,6 @@
/** session info: produced by isabelle build as session log.gz file **/
sealed case class Session_Info(
- session_name: String,
session_timing: Properties.T,
command_timings: List[Properties.T],
ml_statistics: List[Properties.T],
@@ -550,18 +547,11 @@
private def parse_session_info(
log_file: Log_File,
- default_name: String,
command_timings: Boolean,
ml_statistics: Boolean,
task_statistics: Boolean): Session_Info =
{
Session_Info(
- session_name =
- log_file.find_line("\fSession.name = ") match {
- case None => default_name
- case Some(name) if default_name == "" || default_name == name => name
- case Some(name) => log_file.err("log from different session " + quote(name))
- },
session_timing = log_file.find_props("\fTiming = ") getOrElse Nil,
command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil,
ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,
--- a/src/Pure/Thy/sessions.scala Sat Mar 18 22:11:05 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Sun Mar 19 11:56:56 2017 +0100
@@ -629,14 +629,17 @@
/* session info */
def write_session_info(
- db: SQL.Database, build_log: Build_Log.Session_Info, build: Build.Session_Info)
+ db: SQL.Database,
+ session_name: String,
+ build_log: Build_Log.Session_Info,
+ build: Build.Session_Info)
{
db.transaction {
db.drop_table(Session_Info.table)
db.create_table(Session_Info.table)
using(db.insert_statement(Session_Info.table))(stmt =>
{
- db.set_string(stmt, 1, build_log.session_name)
+ db.set_string(stmt, 1, session_name)
db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
db.set_bytes(stmt, 3, compress_properties(build_log.command_timings))
db.set_bytes(stmt, 4, compress_properties(build_log.ml_statistics))
@@ -663,17 +666,11 @@
read_properties(db, Session_Info.table, Session_Info.task_statistics)
def read_build_log(db: SQL.Database,
- default_name: String = "",
command_timings: Boolean = false,
ml_statistics: Boolean = false,
task_statistics: Boolean = false): Build_Log.Session_Info =
{
- val name = read_string(db, Session_Info.table, Session_Info.session_name)
Build_Log.Session_Info(
- session_name =
- if (name == "") default_name
- else if (default_name == "" || default_name == name) name
- else error("Database from different session " + quote(name)),
session_timing = read_session_timing(db),
command_timings = if (command_timings) read_command_timings(db) else Nil,
ml_statistics = if (ml_statistics) read_ml_statistics(db) else Nil,
--- a/src/Pure/Tools/build.ML Sat Mar 18 22:11:05 2017 +0100
+++ b/src/Pure/Tools/build.ML Sun Mar 19 11:56:56 2017 +0100
@@ -168,7 +168,6 @@
let
val symbols = HTML.make_symbols symbol_codes;
- val _ = writeln ("\fSession.name = " ^ name);
val _ =
Session.init
symbols
--- a/src/Pure/Tools/build.scala Sat Mar 18 22:11:05 2017 +0100
+++ b/src/Pure/Tools/build.scala Sun Mar 19 11:56:56 2017 +0100
@@ -49,7 +49,7 @@
try {
using(SQLite.open_database(database))(db =>
{
- val build_log = store.read_build_log(db, name, command_timings = true)
+ val build_log = store.read_build_log(db, command_timings = true)
val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
(build_log.command_timings, session_timing)
})
@@ -500,10 +500,10 @@
database.file.delete
using(SQLite.open_database(database))(db =>
- store.write_session_info(db,
+ store.write_session_info(db, name,
build_log =
Build_Log.Log_File(name, process_result.out_lines).
- parse_session_info(name,
+ parse_session_info(
command_timings = true, ml_statistics = true, task_statistics = true),
build =
Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
--- a/src/Pure/Tools/ml_statistics.scala Sat Mar 18 22:11:05 2017 +0100
+++ b/src/Pure/Tools/ml_statistics.scala Sun Mar 19 11:56:56 2017 +0100
@@ -25,9 +25,6 @@
def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics =
new ML_Statistics(session_name, ml_statistics)
- def apply(info: Build_Log.Session_Info): ML_Statistics =
- apply(info.session_name, info.ml_statistics)
-
val empty = apply("", Nil)
--- a/src/Pure/Tools/task_statistics.scala Sat Mar 18 22:11:05 2017 +0100
+++ b/src/Pure/Tools/task_statistics.scala Sun Mar 19 11:56:56 2017 +0100
@@ -19,9 +19,6 @@
{
def apply(session_name: String, task_statistics: List[Properties.T]): Task_Statistics =
new Task_Statistics(session_name, task_statistics)
-
- def apply(info: Build_Log.Session_Info): Task_Statistics =
- apply(info.session_name, info.task_statistics)
}
final class Task_Statistics private(