src/Pure/Tools/task_statistics.scala
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 65318 342efc382558
permissions -rw-r--r--
tuned signature;
     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(session_name: String, task_statistics: List[Properties.T]): Task_Statistics =
    21     new Task_Statistics(session_name, task_statistics)
    22 }
    23 
    24 final class Task_Statistics private(
    25   val session_name: String, val task_statistics: List[Properties.T])
    26 {
    27   private val Task_Name = new Properties.String("task_name")
    28   private val Run = new Properties.Int("run")
    29 
    30   def chart(bins: Int = 100): JFreeChart =
    31   {
    32     val values = new Array[Double](task_statistics.length)
    33     for ((Run(x), i) <- task_statistics.iterator.zipWithIndex)
    34       values(i) = java.lang.Math.log10((x max 1).toDouble / 1000000)
    35 
    36     val data = new HistogramDataset
    37     data.addSeries("tasks", values, bins)
    38 
    39     val c =
    40       ChartFactory.createHistogram("Task runtime distribution",
    41         "log10(runtime / s)", "number of tasks", data,
    42         PlotOrientation.VERTICAL, true, true, true)
    43 
    44     val renderer = c.getPlot.asInstanceOf[XYPlot].getRenderer.asInstanceOf[XYBarRenderer]
    45     renderer.setMargin(0.1)
    46     renderer.setBarPainter(new StandardXYBarPainter)
    47 
    48     c
    49   }
    50 
    51   def show_frame(bins: Int = 100): Unit =
    52     GUI_Thread.later {
    53       new Frame {
    54         iconImage = GUI.isabelle_image()
    55         title = session_name
    56         contents = Component.wrap(new ChartPanel(chart(bins)))
    57         visible = true
    58       }
    59     }
    60 }
    61