src/Pure/Tools/build_log.scala
changeset 64119 8094eaa38d4b
parent 64117 c2b41b073d8a
child 64120 6c5039016321
     1.1 --- a/src/Pure/Tools/build_log.scala	Sun Oct 09 14:19:46 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Sun Oct 09 15:28:18 2016 +0200
     1.3 @@ -136,8 +136,8 @@
     1.4  
     1.5      /* inlined content */
     1.6  
     1.7 -    def print_props(prefix: String, props: Properties.T): String =
     1.8 -      prefix + YXML.string_of_body(XML.Encode.properties(props))
     1.9 +    def print_props(marker: String, props: Properties.T): String =
    1.10 +      marker + YXML.string_of_body(XML.Encode.properties(props))
    1.11    }
    1.12  
    1.13    class Log_File private(val name: String, val lines: List[String])
    1.14 @@ -191,14 +191,14 @@
    1.15      def parse_props(text: String): Properties.T =
    1.16        xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
    1.17  
    1.18 -    def filter_props(prefix: String): List[Properties.T] =
    1.19 -      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse_props(s)
    1.20 +    def filter_props(marker: String): List[Properties.T] =
    1.21 +      for (line <- lines; s <- Library.try_unprefix(marker, line)) yield parse_props(s)
    1.22  
    1.23 -    def find_line(prefix: String): Option[String] =
    1.24 -      find(Library.try_unprefix(prefix, _))
    1.25 +    def find_line(marker: String): Option[String] =
    1.26 +      find(Library.try_unprefix(marker, _))
    1.27  
    1.28 -    def find_props(prefix: String): Option[Properties.T] =
    1.29 -      find_line(prefix).map(parse_props(_))
    1.30 +    def find_props(marker: String): Option[Properties.T] =
    1.31 +      find_line(marker).map(parse_props(_))
    1.32  
    1.33  
    1.34      /* parse various formats */
    1.35 @@ -300,8 +300,8 @@
    1.36      }
    1.37  
    1.38      log_file.lines match {
    1.39 -      case line :: _ if line.startsWith(Build_History.META_INFO) =>
    1.40 -        Meta_Info(log_file.find_props(Build_History.META_INFO).get,
    1.41 +      case line :: _ if line.startsWith(Build_History.META_INFO_MARKER) =>
    1.42 +        Meta_Info(log_file.find_props(Build_History.META_INFO_MARKER).get,
    1.43            log_file.get_settings(Settings.all_settings))
    1.44  
    1.45        case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>
    1.46 @@ -337,7 +337,10 @@
    1.47  
    1.48  
    1.49  
    1.50 -  /** build info: produced by isabelle build **/
    1.51 +  /** build info: produced by isabelle build or build_history **/
    1.52 +
    1.53 +  val ML_STATISTICS_MARKER = "\fML_statistics = "
    1.54 +  val SESSION_NAME = "session_name"
    1.55  
    1.56    object Session_Status extends Enumeration
    1.57    {
    1.58 @@ -353,6 +356,7 @@
    1.59      threads: Option[Int],
    1.60      timing: Timing,
    1.61      ml_timing: Timing,
    1.62 +    ml_statistics: List[Properties.T],
    1.63      status: Session_Status.Value)
    1.64    {
    1.65      def finished: Boolean = status == Session_Status.FINISHED
    1.66 @@ -369,6 +373,7 @@
    1.67          case None => x
    1.68        }
    1.69  
    1.70 +    def finished_sessions: List[String] = sessions.keySet.iterator.filter(finished(_)).toList
    1.71      def finished(name: String): Boolean = get_default(name, _.finished, false)
    1.72      def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
    1.73      def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
    1.74 @@ -405,9 +410,11 @@
    1.75      var started = Set.empty[String]
    1.76      var failed = Set.empty[String]
    1.77      var cancelled = Set.empty[String]
    1.78 +    var ml_statistics = Map.empty[String, List[Properties.T]]
    1.79 +
    1.80      def all_sessions: Set[String] =
    1.81 -      chapter.keySet ++ groups.keySet ++ threads.keySet ++
    1.82 -      timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled ++ started
    1.83 +      chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++
    1.84 +      ml_timing.keySet ++ failed ++ cancelled ++ started ++ ml_statistics.keySet
    1.85  
    1.86  
    1.87      for (line <- log_file.lines) {
    1.88 @@ -415,21 +422,26 @@
    1.89          case Session_No_Groups(Chapter_Name(chapt, name)) =>
    1.90            chapter += (name -> chapt)
    1.91            groups += (name -> Nil)
    1.92 +
    1.93          case Session_Groups(Chapter_Name(chapt, name), grps) =>
    1.94            chapter += (name -> chapt)
    1.95            groups += (name -> Word.explode(grps))
    1.96 +
    1.97          case Session_Started(name) =>
    1.98            started += name
    1.99 +
   1.100          case Session_Finished1(name,
   1.101              Value.Int(e1), Value.Int(e2), Value.Int(e3),
   1.102              Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
   1.103            val elapsed = Time.hms(e1, e2, e3)
   1.104            val cpu = Time.hms(c1, c2, c3)
   1.105            timing += (name -> Timing(elapsed, cpu, Time.zero))
   1.106 +
   1.107          case Session_Finished2(name,
   1.108              Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
   1.109            val elapsed = Time.hms(e1, e2, e3)
   1.110            timing += (name -> Timing(elapsed, Time.zero, Time.zero))
   1.111 +
   1.112          case Session_Timing(name,
   1.113              Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
   1.114            val elapsed = Time.seconds(e)
   1.115 @@ -437,6 +449,15 @@
   1.116            val gc = Time.seconds(g)
   1.117            ml_timing += (name -> Timing(elapsed, cpu, gc))
   1.118            threads += (name -> t)
   1.119 +
   1.120 +        case _ if line.startsWith(ML_STATISTICS_MARKER) =>
   1.121 +          val (name, props) =
   1.122 +            Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
   1.123 +              case Some((SESSION_NAME, session_name) :: props) => (session_name, props)
   1.124 +              case _ => log_file.err("malformed ML_statistics " + quote(line))
   1.125 +            }
   1.126 +          ml_statistics = ml_statistics + (name -> (props :: ml_statistics.getOrElse(name, Nil)))
   1.127 +
   1.128          case _ =>
   1.129        }
   1.130      }
   1.131 @@ -458,6 +479,7 @@
   1.132                threads.get(name),
   1.133                timing.getOrElse(name, Timing.zero),
   1.134                ml_timing.getOrElse(name, Timing.zero),
   1.135 +              ml_statistics.getOrElse(name, Nil).reverse,
   1.136                status)
   1.137            (name -> entry)
   1.138          }):_*)
   1.139 @@ -494,7 +516,7 @@
   1.140      val command_timings_ =
   1.141        if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
   1.142      val ml_statistics_ =
   1.143 -      if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
   1.144 +      if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil
   1.145      val task_statistics_ =
   1.146        if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
   1.147