src/Pure/Admin/build_log.scala
changeset 66873 9953ae603a23
parent 66863 6acd1a2bd146
child 66874 0b8da0fc9563
     1.1 --- a/src/Pure/Admin/build_log.scala	Mon Oct 16 14:21:14 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Mon Oct 16 14:32:09 2017 +0200
     1.3 @@ -283,9 +283,11 @@
     1.4  
     1.5      def parse_session_info(
     1.6          command_timings: Boolean = false,
     1.7 +        theory_timings: Boolean = false,
     1.8          ml_statistics: Boolean = false,
     1.9          task_statistics: Boolean = false): Session_Info =
    1.10 -      Build_Log.parse_session_info(log_file, command_timings, ml_statistics, task_statistics)
    1.11 +      Build_Log.parse_session_info(
    1.12 +        log_file, command_timings, theory_timings, ml_statistics, task_statistics)
    1.13    }
    1.14  
    1.15  
    1.16 @@ -446,6 +448,7 @@
    1.17  
    1.18    /** build info: toplevel output of isabelle build or Admin/build_history **/
    1.19  
    1.20 +  val THEORY_TIMING_MARKER = "\ftheory_timing = "
    1.21    val ML_STATISTICS_MARKER = "\fML_statistics = "
    1.22    val ERROR_MESSAGE_MARKER = "\ferror_message = "
    1.23    val SESSION_NAME = "session_name"
    1.24 @@ -612,6 +615,7 @@
    1.25    sealed case class Session_Info(
    1.26      session_timing: Properties.T,
    1.27      command_timings: List[Properties.T],
    1.28 +    theory_timings: List[Properties.T],
    1.29      ml_statistics: List[Properties.T],
    1.30      task_statistics: List[Properties.T],
    1.31      errors: List[String])
    1.32 @@ -619,12 +623,14 @@
    1.33    private def parse_session_info(
    1.34      log_file: Log_File,
    1.35      command_timings: Boolean,
    1.36 +    theory_timings: Boolean,
    1.37      ml_statistics: Boolean,
    1.38      task_statistics: Boolean): Session_Info =
    1.39    {
    1.40      Session_Info(
    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 +      theory_timings = if (theory_timings) log_file.filter_props(THEORY_TIMING_MARKER) else Nil,
    1.44        ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,
    1.45        task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil,
    1.46        errors = log_file.filter_lines(ERROR_MESSAGE_MARKER).map(Library.decode_lines(_)))