src/Pure/Admin/build_log.scala
changeset 65318 342efc382558
parent 65290 6c1d7d5c2165
child 65588 b0d8d97198b3
     1.1 --- a/src/Pure/Admin/build_log.scala	Sat Mar 18 22:11:05 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_log.scala	Sun Mar 19 11:56:56 2017 +0100
     1.3 @@ -255,12 +255,10 @@
     1.4      def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
     1.5  
     1.6      def parse_session_info(
     1.7 -        default_name: String = "",
     1.8          command_timings: Boolean = false,
     1.9          ml_statistics: Boolean = false,
    1.10          task_statistics: Boolean = false): Session_Info =
    1.11 -      Build_Log.parse_session_info(
    1.12 -        log_file, default_name, command_timings, ml_statistics, task_statistics)
    1.13 +      Build_Log.parse_session_info(log_file, command_timings, ml_statistics, task_statistics)
    1.14    }
    1.15  
    1.16  
    1.17 @@ -542,7 +540,6 @@
    1.18    /** session info: produced by isabelle build as session log.gz file **/
    1.19  
    1.20    sealed case class Session_Info(
    1.21 -    session_name: String,
    1.22      session_timing: Properties.T,
    1.23      command_timings: List[Properties.T],
    1.24      ml_statistics: List[Properties.T],
    1.25 @@ -550,18 +547,11 @@
    1.26  
    1.27    private def parse_session_info(
    1.28      log_file: Log_File,
    1.29 -    default_name: String,
    1.30      command_timings: Boolean,
    1.31      ml_statistics: Boolean,
    1.32      task_statistics: Boolean): Session_Info =
    1.33    {
    1.34      Session_Info(
    1.35 -      session_name =
    1.36 -        log_file.find_line("\fSession.name = ") match {
    1.37 -          case None => default_name
    1.38 -          case Some(name) if default_name == "" || default_name == name => name
    1.39 -          case Some(name) => log_file.err("log from different session " + quote(name))
    1.40 -        },
    1.41        session_timing = log_file.find_props("\fTiming = ") getOrElse Nil,
    1.42        command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil,
    1.43        ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,