author | wenzelm |
Tue, 13 Jan 2015 21:46:09 +0100 | |
changeset 59362 | 41f1645a4f63 |
parent 57612 | 990ffb84489b |
child 64041 | fd454d9e97c4 |
permissions | -rw-r--r-- |
51240 | 1 |
/* Title: Pure/Tools/task_statistics.scala |
50980 | 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 |
{ |
|
50982 | 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) |
|
50980 | 25 |
} |
26 |
||
50982 | 27 |
final class Task_Statistics private(val name: String, val tasks: List[Properties.T]) |
50980 | 28 |
{ |
50982 | 29 |
private val Task_Name = new Properties.String("task_name") |
30 |
private val Run = new Properties.Int("run") |
|
50980 | 31 |
|
32 |
def chart(bins: Int = 100): JFreeChart = |
|
33 |
{ |
|
50982 | 34 |
val values = new Array[Double](tasks.length) |
51370
716a94cc5aaf
avoid -Infinity which confuses JFreeChart histogram;
wenzelm
parents:
51240
diff
changeset
|
35 |
for ((Run(x), i) <- tasks.iterator.zipWithIndex) |
716a94cc5aaf
avoid -Infinity which confuses JFreeChart histogram;
wenzelm
parents:
51240
diff
changeset
|
36 |
values(i) = java.lang.Math.log10((x max 1).toDouble / 1000000) |
50980 | 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 = |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
51615
diff
changeset
|
54 |
GUI_Thread.later { |
50980 | 55 |
new Frame { |
51615
072a7249e1ac
separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
51370
diff
changeset
|
56 |
iconImage = GUI.isabelle_image() |
50982 | 57 |
title = name |
50980 | 58 |
contents = Component.wrap(new ChartPanel(chart(bins))) |
59 |
visible = true |
|
60 |
} |
|
61 |
} |
|
62 |
} |
|
63 |