src/Pure/ML/ml_statistics.scala

--- a/src/Pure/ML/ml_statistics.scala	Wed Jan 02 19:23:18 2013 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Wed Jan 02 21:02:47 2013 +0100
@@ -9,6 +9,10 @@
 
 import scala.collection.immutable.{SortedSet, SortedMap}
 
+import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
+import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
+import org.jfree.chart.plot.PlotOrientation
+
 
 object ML_Statistics
 {
@@ -59,7 +63,7 @@
   val time_start = ML_Statistics.Now.unapply(stats.head).get
   val duration = ML_Statistics.Now.unapply(stats.last).get - time_start
 
-  val names: Set[String] =
+  val fields: Set[String] =
     SortedSet.empty[String] ++
       (for (props <- stats.iterator; (x, _) <- props.iterator if x != ML_Statistics.Now.name)
         yield x)
@@ -74,5 +78,27 @@
             yield (x, java.lang.Double.parseDouble(y)))
       ML_Statistics.Entry(time, data)
     })
+
+
+  /* charts */
+
+  def chart(title: String, selected_fields: String*): JFreeChart =
+  {
+    val data = new XYSeriesCollection
+
+    for {
+      field <- selected_fields
+      series = new XYSeries(field)
+    } {
+      content.foreach(entry => series.add(entry.time, entry.data(field)))
+      data.addSeries(series)
+    }
+
+    ChartFactory.createXYLineChart(title, "time", "value", data,
+      PlotOrientation.VERTICAL, true, true, true)
+  }
+
+  def chart_panel(title: String, selected_fields: String*): ChartPanel =
+    new ChartPanel(chart(title, selected_fields: _*))
 }