src/Tools/jEdit/src/monitor_dockable.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 55618 995162143ef4
child 56770 e160ae47db94
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
     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.swing.{TextArea, ScrollPane, Component}
    13 
    14 import org.jfree.chart.ChartPanel
    15 import org.jfree.data.xy.XYSeriesCollection
    16 
    17 import org.gjt.sp.jedit.View
    18 
    19 
    20 class Monitor_Dockable(view: View, position: String) extends Dockable(view, position)
    21 {
    22   /* chart data -- owned by Swing thread */
    23 
    24   private val chart = ML_Statistics.empty.chart(null, Nil)
    25   private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
    26   private var rev_stats: List[Properties.T] = Nil
    27 
    28   private val delay_update =
    29     Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
    30       ML_Statistics("", rev_stats.reverse)
    31         .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
    32     }
    33 
    34   set_content(new ChartPanel(chart))
    35 
    36 
    37   /* main */
    38 
    39   private val main =
    40     Session.Consumer[Session.Statistics](getClass.getName) {
    41       case stats =>
    42         Swing_Thread.later {
    43           rev_stats ::= stats.props
    44           delay_update.invoke()
    45         }
    46     }
    47 
    48   override def init() { PIDE.session.statistics += main }
    49   override def exit() { PIDE.session.statistics -= main }
    50 }
    51