equal
deleted
inserted
replaced
7 package isabelle.jedit |
7 package isabelle.jedit |
8 |
8 |
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import scala.actors.Actor._ |
|
13 import scala.swing.{TextArea, ScrollPane, Component} |
12 import scala.swing.{TextArea, ScrollPane, Component} |
14 |
13 |
15 import org.jfree.chart.ChartPanel |
14 import org.jfree.chart.ChartPanel |
16 import org.jfree.data.xy.XYSeriesCollection |
15 import org.jfree.data.xy.XYSeriesCollection |
17 |
16 |
33 } |
32 } |
34 |
33 |
35 set_content(new ChartPanel(chart)) |
34 set_content(new ChartPanel(chart)) |
36 |
35 |
37 |
36 |
38 /* main actor */ |
37 /* main */ |
39 |
38 |
40 private val main_actor = actor { |
39 private val main = |
41 loop { |
40 Session.Consumer[Session.Statistics](getClass.getName) { |
42 react { |
41 case stats => |
43 case Session.Statistics(props) => |
42 Swing_Thread.later { |
44 Swing_Thread.later { |
43 rev_stats ::= stats.props |
45 rev_stats ::= props |
44 delay_update.invoke() |
46 delay_update.invoke() |
45 } |
47 } |
46 } |
48 |
47 |
49 case bad => System.err.println("Monitor_Dockable: ignoring bad message " + bad) |
48 override def init() { PIDE.session.statistics += main } |
50 } |
49 override def exit() { PIDE.session.statistics -= main } |
51 } |
|
52 } |
|
53 |
|
54 override def init() { PIDE.session.statistics += main_actor } |
|
55 override def exit() { PIDE.session.statistics -= main_actor } |
|
56 } |
50 } |
57 |
51 |