# HG changeset patch
# User wenzelm
# Date 1489921016 -3600
# Node ID 342efc382558b0207f1b9defbecc0319b59536d1
# Parent  b9f5cd8456167fb1d0f1ee61b3a3f8ba11cdfc53
eliminated somewhat redundant inlined name (despite a7aa17a1f721);

diff -r b9f5cd845616 -r 342efc382558 src/Pure/Admin/build_history.scala
--- 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)
diff -r b9f5cd845616 -r 342efc382558 src/Pure/Admin/build_log.scala
--- 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,
diff -r b9f5cd845616 -r 342efc382558 src/Pure/Thy/sessions.scala
--- 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,
diff -r b9f5cd845616 -r 342efc382558 src/Pure/Tools/build.ML
--- 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
diff -r b9f5cd845616 -r 342efc382558 src/Pure/Tools/build.scala
--- 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)))
diff -r b9f5cd845616 -r 342efc382558 src/Pure/Tools/ml_statistics.scala
--- 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)
 
 
diff -r b9f5cd845616 -r 342efc382558 src/Pure/Tools/task_statistics.scala
--- 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(