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