31 val empty = apply("", Nil) |
31 val empty = apply("", Nil) |
32 |
32 |
33 |
33 |
34 /* standard fields */ |
34 /* standard fields */ |
35 |
35 |
36 val tasks_fields = |
36 type Fields = (String, Iterable[String]) |
|
37 |
|
38 val tasks_fields: Fields = |
37 ("Future tasks", |
39 ("Future tasks", |
38 List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent")) |
40 List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent")) |
39 |
41 |
40 val workers_fields = |
42 val workers_fields: Fields = |
41 ("Worker threads", List("workers_total", "workers_active", "workers_waiting")) |
43 ("Worker threads", List("workers_total", "workers_active", "workers_waiting")) |
42 |
44 |
43 val GC_fields = ("GCs", List("partial_GCs", "full_GCs")) |
45 val GC_fields: Fields = |
|
46 ("GCs", List("partial_GCs", "full_GCs")) |
44 |
47 |
45 val heap_fields = |
48 val heap_fields: Fields = |
46 ("Heap", List("size_heap", "size_allocation", "size_allocation_free", |
49 ("Heap", List("size_heap", "size_allocation", "size_allocation_free", |
47 "size_heap_free_last_full_GC", "size_heap_free_last_GC")) |
50 "size_heap_free_last_full_GC", "size_heap_free_last_GC")) |
48 |
51 |
49 val threads_fields = |
52 val threads_fields: Fields = |
50 ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", |
53 ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", |
51 "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) |
54 "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) |
52 |
55 |
53 val time_fields = ("Time", List("time_CPU", "time_GC")) |
56 val time_fields: Fields = |
|
57 ("Time", List("time_CPU", "time_GC")) |
54 |
58 |
55 val speed_fields = ("Speed", List("speed_CPU", "speed_GC")) |
59 val speed_fields: Fields = |
|
60 ("Speed", List("speed_CPU", "speed_GC")) |
56 |
61 |
57 val standard_fields = |
62 val standard_fields: List[Fields] = |
58 List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields, |
63 List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields, |
59 time_fields, speed_fields) |
64 time_fields, speed_fields) |
60 } |
65 } |
61 |
66 |
62 final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T]) |
67 final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T]) |
126 |
131 |
127 ChartFactory.createXYLineChart(title, "time", "value", data, |
132 ChartFactory.createXYLineChart(title, "time", "value", data, |
128 PlotOrientation.VERTICAL, true, true, true) |
133 PlotOrientation.VERTICAL, true, true, true) |
129 } |
134 } |
130 |
135 |
131 def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2) |
136 def chart(fields: ML_Statistics.Fields): JFreeChart = |
|
137 chart(fields._1, fields._2) |
132 |
138 |
133 def show_standard_frames(): Unit = |
139 def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.standard_fields): Unit = |
134 ML_Statistics.standard_fields.map(chart(_)).foreach(c => |
140 fields.map(chart(_)).foreach(c => |
135 GUI_Thread.later { |
141 GUI_Thread.later { |
136 new Frame { |
142 new Frame { |
137 iconImage = GUI.isabelle_image() |
143 iconImage = GUI.isabelle_image() |
138 title = session_name |
144 title = session_name |
139 contents = Component.wrap(new ChartPanel(c)) |
145 contents = Component.wrap(new ChartPanel(c)) |