# HG changeset patch
# User wenzelm
# Date 1358544717 -3600
# Node ID bc746aa3e8d5207e51c47d6dfe24b08d2e9557ea
# Parent  21da2a03b9d2cfd9e1ce902008643645b5c6eae4
charts for future task runtime statistics;

diff -r 21da2a03b9d2 -r bc746aa3e8d5 src/Pure/Tools/task_statistics.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/task_statistics.scala	Fri Jan 18 22:31:57 2013 +0100
@@ -0,0 +1,59 @@
+/*  Title:      Pure/ML/task_statistics.ML
+    Author:     Makarius
+
+Future task runtime statistics.
+*/
+
+package isabelle
+
+
+import scala.swing.{Frame, Component}
+
+import org.jfree.data.statistics.HistogramDataset
+import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
+import org.jfree.chart.plot.{XYPlot, PlotOrientation}
+import org.jfree.chart.renderer.xy.{XYBarRenderer, StandardXYBarPainter}
+
+
+object Task_Statistics
+{
+  def apply(stats: List[Properties.T]): Task_Statistics = new Task_Statistics(stats)
+}
+
+final class Task_Statistics private(val stats: List[Properties.T])
+{
+  val Task_Name = new Properties.String("task_name")
+  val Run = new Properties.Int("run")
+
+  def chart(bins: Int = 100): JFreeChart =
+  {
+    val values = new Array[Double](stats.length)
+    for ((Run(x), i) <- stats.iterator.zipWithIndex) values(i) =
+      Math.log10(x.toDouble / 1000000)
+
+    val data = new HistogramDataset
+    data.addSeries("tasks", values, bins)
+
+    val c =
+      ChartFactory.createHistogram("Task runtime distribution",
+        "log10(runtime / s)", "number of tasks", data,
+        PlotOrientation.VERTICAL, true, true, true)
+
+    val renderer = c.getPlot.asInstanceOf[XYPlot].getRenderer.asInstanceOf[XYBarRenderer]
+    renderer.setMargin(0.1)
+    renderer.setBarPainter(new StandardXYBarPainter)
+
+    c
+  }
+
+  def show_frame(bins: Int = 100): Unit =
+    Swing_Thread.later {
+      new Frame {
+        iconImage = Isabelle_System.get_icon().getImage
+        title = "Statistics"
+        contents = Component.wrap(new ChartPanel(chart(bins)))
+        visible = true
+      }
+    }
+}
+
diff -r 21da2a03b9d2 -r bc746aa3e8d5 src/Pure/build-jars
--- a/src/Pure/build-jars	Fri Jan 18 20:31:22 2013 +0100
+++ b/src/Pure/build-jars	Fri Jan 18 22:31:57 2013 +0100
@@ -65,6 +65,7 @@
   Tools/build.scala
   Tools/build_dialog.scala
   Tools/main.scala
+  Tools/task_statistics.scala
   library.scala
   package.scala
   term.scala