author | wenzelm |
Tue, 06 May 2014 22:55:44 +0200 | |
changeset 56886 | 87ebb99786ed |
parent 56770 | e160ae47db94 |
child 57612 | 990ffb84489b |
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 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
4 |
Monitor for runtime statistics. |
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._ |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
11 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
12 |
import scala.swing.{TextArea, ScrollPane, Component} |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
13 |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
14 |
import org.jfree.chart.ChartPanel |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
15 |
import org.jfree.data.xy.XYSeriesCollection |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
16 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
17 |
import org.gjt.sp.jedit.View |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
18 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
19 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
20 |
class Monitor_Dockable(view: View, position: String) extends Dockable(view, position) |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
21 |
{ |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56715
diff
changeset
|
22 |
private val rev_stats = Synchronized(Nil: List[Properties.T]) |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56715
diff
changeset
|
23 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56715
diff
changeset
|
24 |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
25 |
/* chart data -- owned by Swing thread */ |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
26 |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
27 |
private val chart = ML_Statistics.empty.chart(null, Nil) |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
28 |
private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection] |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
29 |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
30 |
private val delay_update = |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
31 |
Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56715
diff
changeset
|
32 |
ML_Statistics("", rev_stats.value.reverse) |
50699 | 33 |
.update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
34 |
} |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
35 |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50433
diff
changeset
|
36 |
set_content(new ChartPanel(chart)) |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
37 |
|
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
38 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
55618
diff
changeset
|
39 |
/* main */ |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
40 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
55618
diff
changeset
|
41 |
private val main = |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
55618
diff
changeset
|
42 |
Session.Consumer[Session.Statistics](getClass.getName) { |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
55618
diff
changeset
|
43 |
case stats => |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56715
diff
changeset
|
44 |
rev_stats.change(stats.props :: _) |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56715
diff
changeset
|
45 |
delay_update.invoke() |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
55618
diff
changeset
|
46 |
} |
53177
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
50982
diff
changeset
|
47 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
55618
diff
changeset
|
48 |
override def init() { PIDE.session.statistics += main } |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
55618
diff
changeset
|
49 |
override def exit() { PIDE.session.statistics -= main } |
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
50 |
} |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff
changeset
|
51 |