src/Pure/ML/ml_statistics.scala
changeset 50777 20126dd9772c
parent 50697 82e9178e6a98
child 50854 2b15227b17e8
equal deleted inserted replaced
50776:5a9964f7a691 50777:20126dd9772c
    20   /* content interpretation */
    20   /* content interpretation */
    21 
    21 
    22   final case class Entry(time: Double, data: Map[String, Double])
    22   final case class Entry(time: Double, data: Map[String, Double])
    23 
    23 
    24   def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
    24   def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
    25   def apply(log: Path): ML_Statistics = apply(read_log(log))
    25   def apply(path: Path): ML_Statistics = apply(Build.parse_log(File.read_gzip(path)).stats)
    26 
    26 
    27   val empty = apply(Nil)
    27   val empty = apply(Nil)
    28 
    28 
    29 
    29 
    30   /* standard fields */
    30   /* standard fields */
    48   val workers_fields =
    48   val workers_fields =
    49     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
    49     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
    50 
    50 
    51   val standard_fields =
    51   val standard_fields =
    52     List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
    52     List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
    53 
       
    54 
       
    55   /* read properties from build log */
       
    56 
       
    57   private val line_prefix = "\fML_statistics = "
       
    58 
       
    59   private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]"
       
    60 
       
    61   private object Parser extends Parse.Parser
       
    62   {
       
    63     private def stat: Parser[(String, String)] =
       
    64       keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^
       
    65       { case _ ~ x ~ _ ~ y ~ _ => (x, y) }
       
    66     private def stats: Parser[Properties.T] =
       
    67       keyword("[") ~> repsep(stat, keyword(",")) <~ keyword("]")
       
    68 
       
    69     def parse_stats(s: String): Properties.T =
       
    70     {
       
    71       parse_all(stats, Token.reader(syntax.scan(s))) match {
       
    72         case Success(result, _) => result
       
    73         case bad => error(bad.toString)
       
    74       }
       
    75     }
       
    76   }
       
    77 
       
    78   def read_log(log: Path): List[Properties.T] =
       
    79     for {
       
    80       line <- split_lines(File.read_gzip(log))
       
    81       if line.startsWith(line_prefix)
       
    82       stats = line.substring(line_prefix.length)
       
    83     } yield Parser.parse_stats(stats)
       
    84 }
    53 }
    85 
    54 
    86 final class ML_Statistics private(val stats: List[Properties.T])
    55 final class ML_Statistics private(val stats: List[Properties.T])
    87 {
    56 {
    88   val Now = new Properties.Double("now")
    57   val Now = new Properties.Double("now")