# HG changeset patch
# User wenzelm
# Date 1493563650 -7200
# Node ID 014dbbe5331f29952717d993dbec4bab37b08d9c
# Parent  2c704ae04db104966f126a625fa86bea2dc10844
parse ml_statistics only when required;

diff -r 2c704ae04db1 -r 014dbbe5331f src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sun Apr 30 16:32:58 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Sun Apr 30 16:47:30 2017 +0200
@@ -202,8 +202,9 @@
           Build_Log.log_filename(Build_History.engine, build_history_date,
             List(build_host, ml_platform, "M" + threads) ::: build_tags)
 
-      val build_info =
-        Build_Log.Log_File(log_path.base.implode, build_result.out_lines).parse_build_info()
+      val build_info: Build_Log.Build_Info =
+        Build_Log.Log_File(log_path.base.implode, build_result.out_lines).
+          parse_build_info(ml_statistics = true)
 
 
       /* output log */
diff -r 2c704ae04db1 -r 014dbbe5331f src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sun Apr 30 16:32:58 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Sun Apr 30 16:47:30 2017 +0200
@@ -272,7 +272,8 @@
 
     def parse_meta_info(): Meta_Info = Build_Log.parse_meta_info(log_file)
 
-    def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
+    def parse_build_info(ml_statistics: Boolean = false): Build_Info =
+      Build_Log.parse_build_info(log_file, ml_statistics)
 
     def parse_session_info(
         command_timings: Boolean = false,
@@ -498,7 +499,7 @@
       get_default(name, entry => ML_Statistics(name, entry.ml_statistics), ML_Statistics.empty)
   }
 
-  private def parse_build_info(log_file: Log_File): Build_Info =
+  private def parse_build_info(log_file: Log_File, parse_ml_statistics: Boolean): Build_Info =
   {
     object Chapter_Name
     {
@@ -574,7 +575,8 @@
         case Heap(name, Value.Long(size)) =>
           heap_sizes += (name -> size)
 
-        case _ if line.startsWith(ML_STATISTICS_MARKER) && YXML.detect(line) =>
+        case _
+        if parse_ml_statistics && line.startsWith(ML_STATISTICS_MARKER) && YXML.detect(line) =>
           val (name, props) =
             Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
               case Some((SESSION_NAME, session_name) :: props) => (session_name, props)
@@ -715,7 +717,7 @@
 
     def update_ml_statistics(db: SQL.Database, log_file: Log_File)
     {
-      val build_info = log_file.parse_build_info()
+      val build_info = log_file.parse_build_info(ml_statistics = true)
       val table = Build_Info.ml_statistics_table
 
       db.transaction {
diff -r 2c704ae04db1 -r 014dbbe5331f src/Pure/Admin/build_stats.scala
--- a/src/Pure/Admin/build_stats.scala	Sun Apr 30 16:32:58 2017 +0200
+++ b/src/Pure/Admin/build_stats.scala	Sun Apr 30 16:47:30 2017 +0200
@@ -29,7 +29,7 @@
 
     val all_infos =
       Par_List.map((job_info: CI_API.Job_Info) =>
-        (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info), job_infos)
+        (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info()), job_infos)
     val all_sessions =
       (Set.empty[String] /: all_infos)(
         { case (s, (_, info)) => s ++ info.sessions.keySet })