11 import isabelle.jedit_base.Dockable |
11 import isabelle.jedit_base.Dockable |
12 |
12 |
13 import java.awt.BorderLayout |
13 import java.awt.BorderLayout |
14 |
14 |
15 import scala.collection.immutable.Queue |
15 import scala.collection.immutable.Queue |
16 import scala.swing.{TextArea, TextField, ScrollPane, Component, ComboBox, Button} |
16 import scala.swing.{TextField, ComboBox, Button} |
17 import scala.swing.event.{SelectionChanged, ButtonClicked, ValueChanged} |
17 import scala.swing.event.{SelectionChanged, ButtonClicked, ValueChanged} |
18 |
18 |
19 import org.jfree.chart.ChartPanel |
19 import org.jfree.chart.ChartPanel |
20 import org.jfree.data.xy.XYSeriesCollection |
20 import org.jfree.data.xy.XYSeriesCollection |
21 |
21 |
46 { |
46 { |
47 statistics = Queue.empty |
47 statistics = Queue.empty |
48 statistics_length = 0 |
48 statistics_length = 0 |
49 } |
49 } |
50 |
50 |
51 private var data_name = ML_Statistics.all_fields(0)._1 |
51 private var data_name = ML_Statistics.all_fields.head._1 |
52 private val chart = ML_Statistics.empty.chart(null, Nil) |
52 private val chart = ML_Statistics.empty.chart(null, Nil) |
53 private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection] |
53 private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection] |
54 |
54 |
55 private def update_chart: Unit = |
55 private def update_chart(): Unit = |
|
56 { |
56 ML_Statistics.all_fields.find(_._1 == data_name) match { |
57 ML_Statistics.all_fields.find(_._1 == data_name) match { |
57 case None => |
58 case None => |
58 case Some((_, fields)) => ML_Statistics(statistics.toList).update_data(data, fields) |
59 case Some((_, fields)) => ML_Statistics(statistics.toList).update_data(data, fields) |
59 } |
60 } |
|
61 } |
60 |
62 |
61 private val input_delay = |
63 private val input_delay = |
62 Delay.first(PIDE.options.seconds("editor_input_delay"), gui = true) { update_chart } |
64 Delay.first(PIDE.options.seconds("editor_input_delay"), gui = true) { update_chart() } |
63 |
65 |
64 private val update_delay = |
66 private val update_delay = |
65 Delay.first(PIDE.options.seconds("editor_chart_delay"), gui = true) { update_chart } |
67 Delay.first(PIDE.options.seconds("editor_chart_delay"), gui = true) { update_chart() } |
66 |
68 |
67 |
69 |
68 /* controls */ |
70 /* controls */ |
69 |
71 |
70 private val select_data = new ComboBox[String](ML_Statistics.all_fields.map(_._1)) |
72 private val select_data = new ComboBox[String](ML_Statistics.all_fields.map(_._1)) |
72 tooltip = "Select visualized data collection" |
74 tooltip = "Select visualized data collection" |
73 listenTo(selection) |
75 listenTo(selection) |
74 reactions += { |
76 reactions += { |
75 case SelectionChanged(_) => |
77 case SelectionChanged(_) => |
76 data_name = selection.item |
78 data_name = selection.item |
77 update_chart |
79 update_chart() |
78 } |
80 } |
79 } |
81 } |
80 |
82 |
81 private val limit_data = new TextField("200", 5) { |
83 private val limit_data = new TextField("200", 5) { |
82 tooltip = "Limit for accumulated data" |
84 tooltip = "Limit for accumulated data" |
83 verifier = (s: String) => |
85 verifier = { |
84 s match { case Value.Int(x) => x > 0 case _ => false } |
86 case Value.Int(x) => x > 0 |
|
87 case _ => false |
|
88 } |
85 reactions += { case ValueChanged(_) => input_delay.invoke() } |
89 reactions += { case ValueChanged(_) => input_delay.invoke() } |
86 } |
90 } |
87 |
91 |
88 private val reset_data = new Button("Reset") { |
92 private val reset_data = new Button("Reset") { |
89 tooltip = "Reset accumulated data" |
93 tooltip = "Reset accumulated data" |
90 reactions += { |
94 reactions += { |
91 case ButtonClicked(_) => clear_statistics() |
95 case ButtonClicked(_) => |
92 update_chart |
96 clear_statistics() |
|
97 update_chart() |
93 } |
98 } |
94 } |
99 } |
95 |
100 |
96 private val full_gc = new Button("GC") { |
101 private val full_gc = new Button("GC") { |
97 tooltip = "Full garbage collection of ML heap" |
102 tooltip = "Full garbage collection of ML heap" |