author | wenzelm |
Thu, 13 Aug 2020 13:13:29 +0200 | |
changeset 72146 | d8dd3aa6dae9 |
parent 72145 | 25db9c4209ee |
child 72147 | 2375b38a42f8 |
permissions | -rw-r--r-- |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/monitor_dockable.scala |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
3 |
|
57869 | 4 |
Monitor for ML statistics. |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
6 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
8 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
9 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
66591
6efa351190d0
more robust: provide docking framework via base plugin;
wenzelm
parents:
66206
diff
changeset
|
11 |
import isabelle.jedit_base.Dockable |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
12 |
|
57869 | 13 |
import java.awt.BorderLayout |
14 |
||
61724
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
15 |
import scala.collection.immutable.Queue |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
16 |
import scala.swing.{TextArea, TextField, ScrollPane, Component, ComboBox, Button} |
61751 | 17 |
import scala.swing.event.{SelectionChanged, ButtonClicked, ValueChanged} |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
18 |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
19 |
import org.jfree.chart.ChartPanel |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
20 |
import org.jfree.data.xy.XYSeriesCollection |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
21 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
22 |
import org.gjt.sp.jedit.View |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
23 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
24 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
25 |
class Monitor_Dockable(view: View, position: String) extends Dockable(view, position) |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
26 |
{ |
61724
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
27 |
/* chart data -- owned by GUI thread */ |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
28 |
|
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
29 |
private var statistics = Queue.empty[Properties.T] |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
30 |
private var statistics_length = 0 |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56715
diff
changeset
|
31 |
|
61724
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
32 |
private def add_statistics(stats: Properties.T) |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
33 |
{ |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
34 |
statistics = statistics.enqueue(stats) |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
35 |
statistics_length += 1 |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
36 |
limit_data.text match { |
63805 | 37 |
case Value.Int(limit) => |
61724
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
38 |
while (statistics_length > limit) { |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
39 |
statistics = statistics.dequeue._2 |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
40 |
statistics_length -= 1 |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
41 |
} |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
42 |
case _ => |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
43 |
} |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
44 |
} |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
45 |
private def clear_statistics() |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
46 |
{ |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
47 |
statistics = Queue.empty |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
48 |
statistics_length = 0 |
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
49 |
} |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
50 |
|
65053 | 51 |
private var data_name = ML_Statistics.all_fields(0)._1 |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
52 |
private val chart = ML_Statistics.empty.chart(null, Nil) |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
53 |
private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection] |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
54 |
|
57869 | 55 |
private def update_chart: Unit = |
65053 | 56 |
ML_Statistics.all_fields.find(_._1 == data_name) match { |
57869 | 57 |
case None => |
65851 | 58 |
case Some((_, fields)) => ML_Statistics(statistics.toList).update_data(data, fields) |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
59 |
} |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
60 |
|
61751 | 61 |
private val input_delay = |
71704 | 62 |
Delay.first(PIDE.options.seconds("editor_input_delay"), gui = true) { update_chart } |
61751 | 63 |
|
64 |
private val update_delay = |
|
71704 | 65 |
Delay.first(PIDE.options.seconds("editor_chart_delay"), gui = true) { update_chart } |
57869 | 66 |
|
67 |
||
68 |
/* controls */ |
|
69 |
||
65053 | 70 |
private val select_data = new ComboBox[String](ML_Statistics.all_fields.map(_._1)) |
57869 | 71 |
{ |
72 |
tooltip = "Select visualized data collection" |
|
73 |
listenTo(selection) |
|
74 |
reactions += { |
|
75 |
case SelectionChanged(_) => |
|
76 |
data_name = selection.item |
|
77 |
update_chart |
|
78 |
} |
|
79 |
} |
|
80 |
||
72145 | 81 |
private val limit_data = new TextField("200", 5) { |
82 |
tooltip = "Limit for accumulated data" |
|
83 |
verifier = (s: String) => |
|
84 |
s match { case Value.Int(x) => x > 0 case _ => false } |
|
85 |
reactions += { case ValueChanged(_) => input_delay.invoke() } |
|
86 |
} |
|
87 |
||
61724
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
88 |
private val reset_data = new Button("Reset") { |
57869 | 89 |
tooltip = "Reset accumulated data" |
90 |
reactions += { |
|
61724
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
91 |
case ButtonClicked(_) => clear_statistics() |
57869 | 92 |
update_chart |
93 |
} |
|
94 |
} |
|
95 |
||
72146 | 96 |
private val full_gc = new Button("GC") { |
97 |
tooltip = "Full garbage collection of ML heap" |
|
98 |
reactions += { |
|
99 |
case ButtonClicked(_) => |
|
100 |
PIDE.session.protocol_command("ML_Heap.full_gc") |
|
101 |
} |
|
102 |
} |
|
103 |
||
104 |
private val share_common_data = new Button("Sharing") { |
|
105 |
tooltip = "Share common data of ML heap" |
|
106 |
reactions += { |
|
107 |
case ButtonClicked(_) => |
|
108 |
PIDE.session.protocol_command("ML_Heap.share_common_data") |
|
109 |
} |
|
110 |
} |
|
111 |
||
112 |
private val controls = |
|
113 |
Wrap_Panel(List(select_data, limit_data, reset_data, full_gc, share_common_data)) |
|
57869 | 114 |
|
115 |
||
116 |
/* layout */ |
|
117 |
||
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
118 |
set_content(new ChartPanel(chart)) |
57869 | 119 |
add(controls.peer, BorderLayout.NORTH) |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
120 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
121 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
55618
diff
changeset
|
122 |
/* main */ |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
123 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
55618
diff
changeset
|
124 |
private val main = |
72135
f67e83608745
removed pointless GUI controls for ML_statistics --- no longer part of prover protocol (see also 38a64cc17403);
wenzelm
parents:
71704
diff
changeset
|
125 |
Session.Consumer[Session.Runtime_Statistics](getClass.getName) { |
f67e83608745
removed pointless GUI controls for ML_statistics --- no longer part of prover protocol (see also 38a64cc17403);
wenzelm
parents:
71704
diff
changeset
|
126 |
case stats => |
61724
4bfcc09a33e8
limit statistics, to avoid exhaustion of heap space or GUI time;
wenzelm
parents:
61590
diff
changeset
|
127 |
add_statistics(stats.props) |
61751 | 128 |
update_delay.invoke() |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
55618
diff
changeset
|
129 |
} |
53177
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
50982
diff
changeset
|
130 |
|
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57869
diff
changeset
|
131 |
override def init() |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57869
diff
changeset
|
132 |
{ |
71652 | 133 |
PIDE.session.runtime_statistics += main |
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57869
diff
changeset
|
134 |
} |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57869
diff
changeset
|
135 |
|
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57869
diff
changeset
|
136 |
override def exit() |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57869
diff
changeset
|
137 |
{ |
71652 | 138 |
PIDE.session.runtime_statistics -= main |
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57869
diff
changeset
|
139 |
} |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
140 |
} |