src/Tools/jEdit/src/monitor_dockable.scala
author wenzelm
Sat Aug 24 13:32:51 2013 +0200 (2013-08-24)
changeset 53177 dcac8d837b9c
parent 50982 a7aa17a1f721
child 55618 995162143ef4
permissions -rw-r--r--
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
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.actors.Actor._
wenzelm@50433
    13
import scala.swing.{TextArea, ScrollPane, Component}
wenzelm@50433
    14
wenzelm@50697
    15
import org.jfree.chart.ChartPanel
wenzelm@50697
    16
import org.jfree.data.xy.XYSeriesCollection
wenzelm@50433
    17
wenzelm@50433
    18
import org.gjt.sp.jedit.View
wenzelm@50433
    19
wenzelm@50433
    20
wenzelm@50433
    21
class Monitor_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@50433
    22
{
wenzelm@50697
    23
  /* chart data -- owned by Swing thread */
wenzelm@50433
    24
wenzelm@50697
    25
  private val chart = ML_Statistics.empty.chart(null, Nil)
wenzelm@50697
    26
  private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
wenzelm@50697
    27
  private var rev_stats: List[Properties.T] = Nil
wenzelm@50433
    28
wenzelm@50697
    29
  private val delay_update =
wenzelm@50697
    30
    Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
wenzelm@50982
    31
      ML_Statistics("", rev_stats.reverse)
wenzelm@50699
    32
        .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
wenzelm@50697
    33
    }
wenzelm@50433
    34
wenzelm@50697
    35
  set_content(new ChartPanel(chart))
wenzelm@50433
    36
wenzelm@50433
    37
wenzelm@50433
    38
  /* main actor */
wenzelm@50433
    39
wenzelm@50433
    40
  private val main_actor = actor {
wenzelm@50433
    41
    loop {
wenzelm@50433
    42
      react {
wenzelm@50697
    43
        case Session.Statistics(props) =>
wenzelm@50697
    44
          Swing_Thread.later {
wenzelm@50697
    45
            rev_stats ::= props
wenzelm@50697
    46
            delay_update.invoke()
wenzelm@50433
    47
          }
wenzelm@53177
    48
wenzelm@50433
    49
        case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad)
wenzelm@50433
    50
      }
wenzelm@50433
    51
    }
wenzelm@50433
    52
  }
wenzelm@50433
    53
wenzelm@50433
    54
  override def init() { PIDE.session.statistics += main_actor }
wenzelm@50433
    55
  override def exit() { PIDE.session.statistics -= main_actor }
wenzelm@50433
    56
}
wenzelm@50433
    57