equal
deleted
inserted
replaced
106 |
106 |
107 /* main */ |
107 /* main */ |
108 |
108 |
109 private val main = |
109 private val main = |
110 Session.Consumer[Any](getClass.getName) { |
110 Session.Consumer[Any](getClass.getName) { |
111 case stats: Session.Statistics => |
111 case stats: Session.Runtime_Statistics => |
112 add_statistics(stats.props) |
112 add_statistics(stats.props) |
113 update_delay.invoke() |
113 update_delay.invoke() |
114 |
114 |
115 case _: Session.Global_Options => |
115 case _: Session.Global_Options => |
116 GUI_Thread.later { ml_stats.load() } |
116 GUI_Thread.later { ml_stats.load() } |
117 } |
117 } |
118 |
118 |
119 override def init() |
119 override def init() |
120 { |
120 { |
121 PIDE.session.statistics += main |
121 PIDE.session.runtime_statistics += main |
122 PIDE.session.global_options += main |
122 PIDE.session.global_options += main |
123 } |
123 } |
124 |
124 |
125 override def exit() |
125 override def exit() |
126 { |
126 { |
127 PIDE.session.statistics -= main |
127 PIDE.session.runtime_statistics -= main |
128 PIDE.session.global_options -= main |
128 PIDE.session.global_options -= main |
129 } |
129 } |
130 } |
130 } |