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;
wenzelm@50433
     1
/*  Title:      Tools/jEdit/src/monitor_dockable.scala
wenzelm@50433
     2
    Author:     Makarius
wenzelm@50433
     3
wenzelm@50433
     4
Monitor for runtime statistics.
wenzelm@50433
     5
*/
wenzelm@50433
     6
wenzelm@50433
     7
package isabelle.jedit
wenzelm@50433
     8
wenzelm@50433
     9
wenzelm@50433
    10
import isabelle._
wenzelm@50433
    11
wenzelm@50433
    12
import scala.swing.{TextArea, ScrollPane, Component}
wenzelm@50433
    13
wenzelm@50697
    14
import org.jfree.chart.ChartPanel
wenzelm@50697
    15
import org.jfree.data.xy.XYSeriesCollection
wenzelm@50433
    16
wenzelm@50433
    17
import org.gjt.sp.jedit.View
wenzelm@50433
    18
wenzelm@50433
    19
wenzelm@50433
    20
class Monitor_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@50433
    21
{
wenzelm@50697
    22
  /* chart data -- owned by Swing thread */
wenzelm@50433
    23
wenzelm@50697
    24
  private val chart = ML_Statistics.empty.chart(null, Nil)
wenzelm@50697
    25
  private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
wenzelm@50697
    26
  private var rev_stats: List[Properties.T] = Nil
wenzelm@50433
    27
wenzelm@50697
    28
  private val delay_update =
wenzelm@50697
    29
    Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
wenzelm@50982
    30
      ML_Statistics("", rev_stats.reverse)
wenzelm@50699
    31
        .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
wenzelm@50697
    32
    }
wenzelm@50433
    33
wenzelm@50697
    34
  set_content(new ChartPanel(chart))
wenzelm@50433
    35
wenzelm@50433
    36
wenzelm@56715
    37
  /* main */
wenzelm@50433
    38
wenzelm@56715
    39
  private val main =
wenzelm@56715
    40
    Session.Consumer[Session.Statistics](getClass.getName) {
wenzelm@56715
    41
      case stats =>
wenzelm@56715
    42
        Swing_Thread.later {
wenzelm@56715
    43
          rev_stats ::= stats.props
wenzelm@56715
    44
          delay_update.invoke()
wenzelm@56715
    45
        }
wenzelm@56715
    46
    }
wenzelm@53177
    47
wenzelm@56715
    48
  override def init() { PIDE.session.statistics += main }
wenzelm@56715
    49
  override def exit() { PIDE.session.statistics -= main }
wenzelm@50433
    50
}
wenzelm@50433
    51