src/Tools/jEdit/src/monitor_dockable.scala
author wenzelm
Fri, 06 Nov 2015 18:15:35 +0100
changeset 61590 94ab348eaab2
parent 60074 38a64cc17403
child 61724 4bfcc09a33e8
permissions -rw-r--r--
tuned;
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
{
61590
wenzelm
parents: 60074
diff changeset
    25
  private val rev_stats = Synchronized[List[Properties.T]](Nil)
56770
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
60074
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    47
  private val ml_stats = new Isabelle.ML_Stats
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    48
57869
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    49
  private val select_data = new ComboBox[String](
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    50
    ML_Statistics.standard_fields.map(_._1))
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    51
  {
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    52
    tooltip = "Select visualized data collection"
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    53
    listenTo(selection)
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    54
    reactions += {
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    55
      case SelectionChanged(_) =>
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    56
        data_name = selection.item
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    57
        update_chart
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    58
    }
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    59
  }
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    60
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    61
  val reset_data = new Button("Reset") {
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    62
    tooltip = "Reset accumulated data"
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    63
    reactions += {
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    64
      case ButtonClicked(_) =>
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    65
        rev_stats.change(_ => Nil)
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    66
        update_chart
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    67
    }
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    68
  }
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    69
60074
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    70
  private val controls =
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    71
    new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats, select_data, reset_data)
57869
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    72
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    73
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    74
  /* layout */
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    75
50697
82e9178e6a98 improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents: 50433
diff changeset
    76
  set_content(new ChartPanel(chart))
57869
9665f79a7181 improved monitor panel;
wenzelm
parents: 57612
diff changeset
    77
  add(controls.peer, BorderLayout.NORTH)
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    78
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    79
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 55618
diff changeset
    80
  /* main */
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
    81
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 55618
diff changeset
    82
  private val main =
60074
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    83
    Session.Consumer[Any](getClass.getName) {
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    84
      case stats: Session.Statistics =>
56770
e160ae47db94 mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents: 56715
diff changeset
    85
        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
    86
        delay_update.invoke()
60074
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    87
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    88
      case _: Session.Global_Options =>
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    89
        GUI_Thread.later { ml_stats.load() }
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 55618
diff changeset
    90
    }
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 50982
diff changeset
    91
60074
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    92
  override def init()
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    93
  {
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    94
    PIDE.session.statistics += main
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    95
    PIDE.session.global_options += main
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    96
  }
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    97
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    98
  override def exit()
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
    99
  {
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
   100
    PIDE.session.statistics -= main
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
   101
    PIDE.session.global_options -= main
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 57869
diff changeset
   102
  }
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
diff changeset
   103
}