eliminated somewhat redundant inlined name (despite a7aa17a1f721);
authorwenzelm
Sun Mar 19 11:56:56 2017 +0100 (2017-03-19)
changeset 65318342efc382558
parent 65317 b9f5cd845616
child 65319 64da14387b2c
eliminated somewhat redundant inlined name (despite a7aa17a1f721);
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_log.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/Tools/ml_statistics.scala
src/Pure/Tools/task_statistics.scala
     1.1 --- a/src/Pure/Admin/build_history.scala	Sat Mar 18 22:11:05 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_history.scala	Sun Mar 19 11:56:56 2017 +0100
     1.3 @@ -230,11 +230,10 @@
     1.4              val properties =
     1.5                if (database.is_file) {
     1.6                  using(SQLite.open_database(database))(db =>
     1.7 -                  store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
     1.8 +                  store.read_build_log(db, ml_statistics = true)).ml_statistics
     1.9                }
    1.10                else if (log_gz.is_file) {
    1.11 -                Build_Log.Log_File(log_gz).
    1.12 -                  parse_session_info(session_name, ml_statistics = true).ml_statistics
    1.13 +                Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
    1.14                }
    1.15                else Nil
    1.16              properties.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
     2.1 --- a/src/Pure/Admin/build_log.scala	Sat Mar 18 22:11:05 2017 +0100
     2.2 +++ b/src/Pure/Admin/build_log.scala	Sun Mar 19 11:56:56 2017 +0100
     2.3 @@ -255,12 +255,10 @@
     2.4      def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
     2.5  
     2.6      def parse_session_info(
     2.7 -        default_name: String = "",
     2.8          command_timings: Boolean = false,
     2.9          ml_statistics: Boolean = false,
    2.10          task_statistics: Boolean = false): Session_Info =
    2.11 -      Build_Log.parse_session_info(
    2.12 -        log_file, default_name, command_timings, ml_statistics, task_statistics)
    2.13 +      Build_Log.parse_session_info(log_file, command_timings, ml_statistics, task_statistics)
    2.14    }
    2.15  
    2.16  
    2.17 @@ -542,7 +540,6 @@
    2.18    /** session info: produced by isabelle build as session log.gz file **/
    2.19  
    2.20    sealed case class Session_Info(
    2.21 -    session_name: String,
    2.22      session_timing: Properties.T,
    2.23      command_timings: List[Properties.T],
    2.24      ml_statistics: List[Properties.T],
    2.25 @@ -550,18 +547,11 @@
    2.26  
    2.27    private def parse_session_info(
    2.28      log_file: Log_File,
    2.29 -    default_name: String,
    2.30      command_timings: Boolean,
    2.31      ml_statistics: Boolean,
    2.32      task_statistics: Boolean): Session_Info =
    2.33    {
    2.34      Session_Info(
    2.35 -      session_name =
    2.36 -        log_file.find_line("\fSession.name = ") match {
    2.37 -          case None => default_name
    2.38 -          case Some(name) if default_name == "" || default_name == name => name
    2.39 -          case Some(name) => log_file.err("log from different session " + quote(name))
    2.40 -        },
    2.41        session_timing = log_file.find_props("\fTiming = ") getOrElse Nil,
    2.42        command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil,
    2.43        ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,
     3.1 --- a/src/Pure/Thy/sessions.scala	Sat Mar 18 22:11:05 2017 +0100
     3.2 +++ b/src/Pure/Thy/sessions.scala	Sun Mar 19 11:56:56 2017 +0100
     3.3 @@ -629,14 +629,17 @@
     3.4      /* session info */
     3.5  
     3.6      def write_session_info(
     3.7 -      db: SQL.Database, build_log: Build_Log.Session_Info, build: Build.Session_Info)
     3.8 +      db: SQL.Database,
     3.9 +      session_name: String,
    3.10 +      build_log: Build_Log.Session_Info,
    3.11 +      build: Build.Session_Info)
    3.12      {
    3.13        db.transaction {
    3.14          db.drop_table(Session_Info.table)
    3.15          db.create_table(Session_Info.table)
    3.16          using(db.insert_statement(Session_Info.table))(stmt =>
    3.17          {
    3.18 -          db.set_string(stmt, 1, build_log.session_name)
    3.19 +          db.set_string(stmt, 1, session_name)
    3.20            db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
    3.21            db.set_bytes(stmt, 3, compress_properties(build_log.command_timings))
    3.22            db.set_bytes(stmt, 4, compress_properties(build_log.ml_statistics))
    3.23 @@ -663,17 +666,11 @@
    3.24        read_properties(db, Session_Info.table, Session_Info.task_statistics)
    3.25  
    3.26      def read_build_log(db: SQL.Database,
    3.27 -      default_name: String = "",
    3.28        command_timings: Boolean = false,
    3.29        ml_statistics: Boolean = false,
    3.30        task_statistics: Boolean = false): Build_Log.Session_Info =
    3.31      {
    3.32 -      val name = read_string(db, Session_Info.table, Session_Info.session_name)
    3.33        Build_Log.Session_Info(
    3.34 -        session_name =
    3.35 -          if (name == "") default_name
    3.36 -          else if (default_name == "" || default_name == name) name
    3.37 -          else error("Database from different session " + quote(name)),
    3.38          session_timing = read_session_timing(db),
    3.39          command_timings = if (command_timings) read_command_timings(db) else Nil,
    3.40          ml_statistics = if (ml_statistics) read_ml_statistics(db) else Nil,
     4.1 --- a/src/Pure/Tools/build.ML	Sat Mar 18 22:11:05 2017 +0100
     4.2 +++ b/src/Pure/Tools/build.ML	Sun Mar 19 11:56:56 2017 +0100
     4.3 @@ -168,7 +168,6 @@
     4.4    let
     4.5      val symbols = HTML.make_symbols symbol_codes;
     4.6  
     4.7 -    val _ = writeln ("\fSession.name = " ^ name);
     4.8      val _ =
     4.9        Session.init
    4.10          symbols
     5.1 --- a/src/Pure/Tools/build.scala	Sat Mar 18 22:11:05 2017 +0100
     5.2 +++ b/src/Pure/Tools/build.scala	Sun Mar 19 11:56:56 2017 +0100
     5.3 @@ -49,7 +49,7 @@
     5.4            try {
     5.5              using(SQLite.open_database(database))(db =>
     5.6              {
     5.7 -              val build_log = store.read_build_log(db, name, command_timings = true)
     5.8 +              val build_log = store.read_build_log(db, command_timings = true)
     5.9                val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
    5.10                (build_log.command_timings, session_timing)
    5.11              })
    5.12 @@ -500,10 +500,10 @@
    5.13                database.file.delete
    5.14  
    5.15                using(SQLite.open_database(database))(db =>
    5.16 -                store.write_session_info(db,
    5.17 +                store.write_session_info(db, name,
    5.18                    build_log =
    5.19                      Build_Log.Log_File(name, process_result.out_lines).
    5.20 -                      parse_session_info(name,
    5.21 +                      parse_session_info(
    5.22                          command_timings = true, ml_statistics = true, task_statistics = true),
    5.23                    build =
    5.24                      Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
     6.1 --- a/src/Pure/Tools/ml_statistics.scala	Sat Mar 18 22:11:05 2017 +0100
     6.2 +++ b/src/Pure/Tools/ml_statistics.scala	Sun Mar 19 11:56:56 2017 +0100
     6.3 @@ -25,9 +25,6 @@
     6.4    def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics =
     6.5      new ML_Statistics(session_name, ml_statistics)
     6.6  
     6.7 -  def apply(info: Build_Log.Session_Info): ML_Statistics =
     6.8 -    apply(info.session_name, info.ml_statistics)
     6.9 -
    6.10    val empty = apply("", Nil)
    6.11  
    6.12  
     7.1 --- a/src/Pure/Tools/task_statistics.scala	Sat Mar 18 22:11:05 2017 +0100
     7.2 +++ b/src/Pure/Tools/task_statistics.scala	Sun Mar 19 11:56:56 2017 +0100
     7.3 @@ -19,9 +19,6 @@
     7.4  {
     7.5    def apply(session_name: String, task_statistics: List[Properties.T]): Task_Statistics =
     7.6      new Task_Statistics(session_name, task_statistics)
     7.7 -
     7.8 -  def apply(info: Build_Log.Session_Info): Task_Statistics =
     7.9 -    apply(info.session_name, info.task_statistics)
    7.10  }
    7.11  
    7.12  final class Task_Statistics private(