src/Tools/jEdit/src/monitor_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 63805 c272680df665
child 65053 460f0fd2f77a
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/jEdit/src/monitor_dockable.scala
     2     Author:     Makarius
     3 
     4 Monitor for ML statistics.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.BorderLayout
    13 
    14 import scala.collection.immutable.Queue
    15 import scala.swing.{TextArea, TextField, ScrollPane, Component, ComboBox, Button}
    16 import scala.swing.event.{SelectionChanged, ButtonClicked, ValueChanged}
    17 
    18 import org.jfree.chart.ChartPanel
    19 import org.jfree.data.xy.XYSeriesCollection
    20 
    21 import org.gjt.sp.jedit.View
    22 
    23 
    24 class Monitor_Dockable(view: View, position: String) extends Dockable(view, position)
    25 {
    26   /* chart data -- owned by GUI thread */
    27 
    28   private var statistics = Queue.empty[Properties.T]
    29   private var statistics_length = 0
    30 
    31   private def add_statistics(stats: Properties.T)
    32   {
    33     statistics = statistics.enqueue(stats)
    34     statistics_length += 1
    35     limit_data.text match {
    36       case Value.Int(limit) =>
    37         while (statistics_length > limit) {
    38           statistics = statistics.dequeue._2
    39           statistics_length -= 1
    40         }
    41       case _ =>
    42     }
    43   }
    44   private def clear_statistics()
    45   {
    46     statistics = Queue.empty
    47     statistics_length = 0
    48   }
    49 
    50   private var data_name = ML_Statistics.standard_fields(0)._1
    51   private val chart = ML_Statistics.empty.chart(null, Nil)
    52   private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
    53 
    54   private def update_chart: Unit =
    55     ML_Statistics.standard_fields.find(_._1 == data_name) match {
    56       case None =>
    57       case Some((_, fields)) => ML_Statistics("", statistics.toList).update_data(data, fields)
    58     }
    59 
    60   private val input_delay =
    61     GUI_Thread.delay_first(PIDE.options.seconds("editor_input_delay")) { update_chart }
    62 
    63   private val update_delay =
    64     GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart }
    65 
    66 
    67   /* controls */
    68 
    69   private val ml_stats = new Isabelle.ML_Stats
    70 
    71   private val select_data = new ComboBox[String](
    72     ML_Statistics.standard_fields.map(_._1))
    73   {
    74     tooltip = "Select visualized data collection"
    75     listenTo(selection)
    76     reactions += {
    77       case SelectionChanged(_) =>
    78         data_name = selection.item
    79         update_chart
    80     }
    81   }
    82 
    83   private val reset_data = new Button("Reset") {
    84     tooltip = "Reset accumulated data"
    85     reactions += {
    86       case ButtonClicked(_) => clear_statistics()
    87         update_chart
    88     }
    89   }
    90 
    91   private val limit_data = new TextField("200", 5) {
    92     tooltip = "Limit for accumulated data"
    93     verifier = (s: String) =>
    94       s match { case Value.Int(x) => x > 0 case _ => false }
    95     reactions += { case ValueChanged(_) => input_delay.invoke() }
    96   }
    97 
    98   private val controls =
    99     new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats, select_data, reset_data, limit_data)
   100 
   101 
   102   /* layout */
   103 
   104   set_content(new ChartPanel(chart))
   105   add(controls.peer, BorderLayout.NORTH)
   106 
   107 
   108   /* main */
   109 
   110   private val main =
   111     Session.Consumer[Any](getClass.getName) {
   112       case stats: Session.Statistics =>
   113         add_statistics(stats.props)
   114         update_delay.invoke()
   115 
   116       case _: Session.Global_Options =>
   117         GUI_Thread.later { ml_stats.load() }
   118     }
   119 
   120   override def init()
   121   {
   122     PIDE.session.statistics += main
   123     PIDE.session.global_options += main
   124   }
   125 
   126   override def exit()
   127   {
   128     PIDE.session.statistics -= main
   129     PIDE.session.global_options -= main
   130   }
   131 }