src/Pure/Tools/task_statistics.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 51615 072a7249e1ac
child 64041 fd454d9e97c4
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
     1 /*  Title:      Pure/Tools/task_statistics.scala
     2     Author:     Makarius
     3 
     4 Future task runtime statistics.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.swing.{Frame, Component}
    11 
    12 import org.jfree.data.statistics.HistogramDataset
    13 import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
    14 import org.jfree.chart.plot.{XYPlot, PlotOrientation}
    15 import org.jfree.chart.renderer.xy.{XYBarRenderer, StandardXYBarPainter}
    16 
    17 
    18 object Task_Statistics
    19 {
    20   def apply(name: String, tasks: List[Properties.T]): Task_Statistics =
    21     new Task_Statistics(name, tasks)
    22 
    23   def apply(info: Build.Log_Info): Task_Statistics =
    24     apply(info.name, info.tasks)
    25 }
    26 
    27 final class Task_Statistics private(val name: String, val tasks: List[Properties.T])
    28 {
    29   private val Task_Name = new Properties.String("task_name")
    30   private val Run = new Properties.Int("run")
    31 
    32   def chart(bins: Int = 100): JFreeChart =
    33   {
    34     val values = new Array[Double](tasks.length)
    35     for ((Run(x), i) <- tasks.iterator.zipWithIndex)
    36       values(i) = java.lang.Math.log10((x max 1).toDouble / 1000000)
    37 
    38     val data = new HistogramDataset
    39     data.addSeries("tasks", values, bins)
    40 
    41     val c =
    42       ChartFactory.createHistogram("Task runtime distribution",
    43         "log10(runtime / s)", "number of tasks", data,
    44         PlotOrientation.VERTICAL, true, true, true)
    45 
    46     val renderer = c.getPlot.asInstanceOf[XYPlot].getRenderer.asInstanceOf[XYBarRenderer]
    47     renderer.setMargin(0.1)
    48     renderer.setBarPainter(new StandardXYBarPainter)
    49 
    50     c
    51   }
    52 
    53   def show_frame(bins: Int = 100): Unit =
    54     GUI_Thread.later {
    55       new Frame {
    56         iconImage = GUI.isabelle_image()
    57         title = name
    58         contents = Component.wrap(new ChartPanel(chart(bins)))
    59         visible = true
    60       }
    61     }
    62 }
    63