src/Tools/jEdit/src/monitor_dockable.scala
author wenzelm
Mon Apr 28 14:41:49 2014 +0200 (2014-04-28)
changeset 56770 e160ae47db94
parent 56715 52125652e82a
child 57612 990ffb84489b
permissions -rw-r--r--
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
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@56770
    22
  private val rev_stats = Synchronized(Nil: List[Properties.T])
wenzelm@56770
    23
wenzelm@56770
    24
wenzelm@50697
    25
  /* chart data -- owned by Swing thread */
wenzelm@50433
    26
wenzelm@50697
    27
  private val chart = ML_Statistics.empty.chart(null, Nil)
wenzelm@50697
    28
  private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
wenzelm@50433
    29
wenzelm@50697
    30
  private val delay_update =
wenzelm@50697
    31
    Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
wenzelm@56770
    32
      ML_Statistics("", rev_stats.value.reverse)
wenzelm@50699
    33
        .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
wenzelm@50697
    34
    }
wenzelm@50433
    35
wenzelm@50697
    36
  set_content(new ChartPanel(chart))
wenzelm@50433
    37
wenzelm@50433
    38
wenzelm@56715
    39
  /* main */
wenzelm@50433
    40
wenzelm@56715
    41
  private val main =
wenzelm@56715
    42
    Session.Consumer[Session.Statistics](getClass.getName) {
wenzelm@56715
    43
      case stats =>
wenzelm@56770
    44
        rev_stats.change(stats.props :: _)
wenzelm@56770
    45
        delay_update.invoke()
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