|
1 /* Title: Tools/jEdit/src/monitor_dockable.scala |
|
2 Author: Makarius |
|
3 |
|
4 Monitor for runtime statistics. |
|
5 */ |
|
6 |
|
7 package isabelle.jedit |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import scala.actors.Actor._ |
|
13 import scala.swing.{TextArea, ScrollPane, Component} |
|
14 |
|
15 import org.jfree.chart.{ChartFactory, ChartPanel} |
|
16 import org.jfree.data.time.{Millisecond, TimeSeries, TimeSeriesCollection} |
|
17 |
|
18 import org.gjt.sp.jedit.View |
|
19 |
|
20 |
|
21 class Monitor_Dockable(view: View, position: String) extends Dockable(view, position) |
|
22 { |
|
23 /* properties */ // FIXME avoid hardwired stuff |
|
24 |
|
25 private val Now = new Properties.Double("now") |
|
26 private val Size_Heap = new Properties.Double("size_heap") |
|
27 |
|
28 private val series = new TimeSeries("ML heap size", classOf[Millisecond]) |
|
29 |
|
30 |
|
31 /* chart */ |
|
32 |
|
33 private val chart_panel = |
|
34 { |
|
35 val data = new TimeSeriesCollection(series) |
|
36 val chart = ChartFactory.createTimeSeriesChart(null, "Time", "Value", data, true, true, false) |
|
37 val plot = chart.getXYPlot() |
|
38 |
|
39 val x_axis = plot.getDomainAxis() |
|
40 x_axis.setAutoRange(true) |
|
41 x_axis.setFixedAutoRange(60000.0) |
|
42 |
|
43 val y_axis = plot.getRangeAxis() |
|
44 y_axis.setAutoRange(true) |
|
45 |
|
46 new ChartPanel(chart) |
|
47 } |
|
48 set_content(chart_panel) |
|
49 |
|
50 |
|
51 /* main actor */ |
|
52 |
|
53 private val main_actor = actor { |
|
54 var t0: Option[Double] = None |
|
55 loop { |
|
56 react { |
|
57 case Session.Statistics(stats) => |
|
58 java.lang.System.err.println(stats) |
|
59 stats match { |
|
60 case Now(t1) => |
|
61 if (t0.isEmpty) t0 = Some(t1) |
|
62 val t = t1 - t0.get |
|
63 stats match { |
|
64 case Size_Heap(x) => series.add(new Millisecond(), x) // FIXME proper time point |
|
65 case _ => |
|
66 } |
|
67 case _ => |
|
68 } |
|
69 case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad) |
|
70 } |
|
71 } |
|
72 } |
|
73 |
|
74 override def init() { PIDE.session.statistics += main_actor } |
|
75 override def exit() { PIDE.session.statistics -= main_actor } |
|
76 } |
|
77 |