# HG changeset patch
# User wenzelm
# Date 1357159194 -3600
# Node ID 03c4d75e8e32e10d829eca1b39364cf1e9013c3b
# Parent  0607d557d073591e3939b08d2b9e6456ec82f402
some grouping of standard fields;
tuned signature;

diff -r 0607d557d073 -r 03c4d75e8e32 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed Jan 02 21:02:47 2013 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Wed Jan 02 21:39:54 2013 +0100
@@ -16,6 +16,39 @@
 
 object ML_Statistics
 {
+  /* content interpretation */
+
+  final case class Entry(time: Double, data: Map[String, Double])
+
+  def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
+  def apply(log: Path): ML_Statistics = apply(read_log(log))
+
+
+  /* standard fields */
+
+  val GC_fields = ("GCs", List("partial_GCs", "full_GCs"))
+
+  val heap_fields =
+    ("Heap", List("size_heap", "size_allocation", "size_allocation_free",
+      "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
+
+  val threads_fields =
+    ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
+      "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
+
+  val time_fields =
+    ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
+
+  val tasks_fields =
+    ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
+
+  val workers_fields =
+    ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
+
+  val standard_fields =
+    List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
+
+
   /* read properties from build log */
 
   private val line_prefix = "\fML_statistics = "
@@ -45,36 +78,29 @@
       if line.startsWith(line_prefix)
       stats = line.substring(line_prefix.length)
     } yield Parser.parse_stats(stats)
-
-
-  /* content interpretation */
-
-  val Now = new Properties.Double("now")
-  final case class Entry(time: Double, data: Map[String, Double])
-
-  def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
-  def apply(log: Path): ML_Statistics = apply(read_log(log))
 }
 
 final class ML_Statistics private(val stats: List[Properties.T])
 {
-  require(!stats.isEmpty && stats.forall(props => ML_Statistics.Now.unapply(props).isDefined))
+  val Now = new Properties.Double("now")
 
-  val time_start = ML_Statistics.Now.unapply(stats.head).get
-  val duration = ML_Statistics.Now.unapply(stats.last).get - time_start
+  require(!stats.isEmpty && stats.forall(props => Now.unapply(props).isDefined))
+
+  val time_start = Now.unapply(stats.head).get
+  val duration = Now.unapply(stats.last).get - time_start
 
   val fields: Set[String] =
     SortedSet.empty[String] ++
-      (for (props <- stats.iterator; (x, _) <- props.iterator if x != ML_Statistics.Now.name)
+      (for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name)
         yield x)
 
   val content: List[ML_Statistics.Entry] =
     stats.map(props => {
-      val time = ML_Statistics.Now.unapply(props).get - time_start
+      val time = Now.unapply(props).get - time_start
       require(time >= 0.0)
       val data =
         SortedMap.empty[String, Double] ++
-          (for ((x, y) <- props.iterator if x != ML_Statistics.Now.name)
+          (for ((x, y) <- props.iterator if x != Now.name)
             yield (x, java.lang.Double.parseDouble(y)))
       ML_Statistics.Entry(time, data)
     })
@@ -82,12 +108,12 @@
 
   /* charts */
 
-  def chart(title: String, selected_fields: String*): JFreeChart =
+  def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
   {
     val data = new XYSeriesCollection
 
     for {
-      field <- selected_fields
+      field <- selected_fields.iterator
       series = new XYSeries(field)
     } {
       content.foreach(entry => series.add(entry.time, entry.data(field)))
@@ -98,7 +124,7 @@
       PlotOrientation.VERTICAL, true, true, true)
   }
 
-  def chart_panel(title: String, selected_fields: String*): ChartPanel =
-    new ChartPanel(chart(title, selected_fields: _*))
+  def chart_panel(title: String, selected_fields: Iterable[String]): ChartPanel =
+    new ChartPanel(chart(title, selected_fields))
 }