src/Tools/jEdit/src/monitor_dockable.scala
author wenzelm
Fri, 08 Aug 2014 11:43:08 +0200
changeset 57869 9665f79a7181
parent 57612 990ffb84489b
child 60074 38a64cc17403
permissions -rw-r--r--
improved monitor panel;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/monitor_dockable.scala
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
     3
57869
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
     4
Monitor for ML statistics.
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
     5
*/
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
     6
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
     8
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
     9
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    10
import isabelle._
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    11
57869
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    12
import java.awt.BorderLayout
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    13
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    14
import scala.swing.{TextArea, ScrollPane, Component, ComboBox, Button}
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    15
import scala.swing.event.{SelectionChanged, ButtonClicked}
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    16
50697
82e9178e6a98 improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents: 50433
diff changeset
    17
import org.jfree.chart.ChartPanel
82e9178e6a98 improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents: 50433
diff changeset
    18
import org.jfree.data.xy.XYSeriesCollection
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    19
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    20
import org.gjt.sp.jedit.View
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    21
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    22
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    23
class Monitor_Dockable(view: View, position: String) extends Dockable(view, position)
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    24
{
56770
e160ae47db94 mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents: 56715
diff changeset
    25
  private val rev_stats = Synchronized(Nil: List[Properties.T])
e160ae47db94 mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents: 56715
diff changeset
    26
e160ae47db94 mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents: 56715
diff changeset
    27
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56770
diff changeset
    28
  /* chart data -- owned by GUI thread */
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    29
57869
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    30
  private var data_name = ML_Statistics.standard_fields(0)._1
50697
82e9178e6a98 improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents: 50433
diff changeset
    31
  private val chart = ML_Statistics.empty.chart(null, Nil)
82e9178e6a98 improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents: 50433
diff changeset
    32
  private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    33
57869
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    34
  private def update_chart: Unit =
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    35
    ML_Statistics.standard_fields.find(_._1 == data_name) match {
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    36
      case None =>
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    37
      case Some((_, fields)) =>
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    38
        ML_Statistics("", rev_stats.value.reverse).update_data(data, fields)
50697
82e9178e6a98 improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents: 50433
diff changeset
    39
    }
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    40
57869
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    41
  private val delay_update =
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    42
    GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart }
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    43
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    44
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    45
  /* controls */
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    46
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    47
  private val select_data = new ComboBox[String](
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    48
    ML_Statistics.standard_fields.map(_._1))
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    49
  {
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    50
    tooltip = "Select visualized data collection"
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    51
    listenTo(selection)
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    52
    reactions += {
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    53
      case SelectionChanged(_) =>
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    54
        data_name = selection.item
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    55
        update_chart
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    56
    }
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    57
  }
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    58
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    59
  val reset_data = new Button("Reset") {
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    60
    tooltip = "Reset accumulated data"
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    61
    reactions += {
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    62
      case ButtonClicked(_) =>
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    63
        rev_stats.change(_ => Nil)
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    64
        update_chart
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    65
    }
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    66
  }
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    67
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    68
  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(select_data, reset_data)
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    69
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    70
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    71
  /* layout */
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    72
50697
82e9178e6a98 improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents: 50433
diff changeset
    73
  set_content(new ChartPanel(chart))
57869
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    74
  add(controls.peer, BorderLayout.NORTH)
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    75
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    76
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 55618
diff changeset
    77
  /* main */
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    78
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 55618
diff changeset
    79
  private val main =
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 55618
diff changeset
    80
    Session.Consumer[Session.Statistics](getClass.getName) {
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 55618
diff changeset
    81
      case stats =>
56770
e160ae47db94 mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents: 56715
diff changeset
    82
        rev_stats.change(stats.props :: _)
e160ae47db94 mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents: 56715
diff changeset
    83
        delay_update.invoke()
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 55618
diff changeset
    84
    }
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 50982
diff changeset
    85
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 55618
diff changeset
    86
  override def init() { PIDE.session.statistics += main }
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 55618
diff changeset
    87
  override def exit() { PIDE.session.statistics -= main }
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    88
}
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    89