improved Monitor_Dockable, based on ML_Statistics operations;
authorwenzelm
Thu Jan 03 13:54:45 2013 +0100 (2013-01-03)
changeset 5069782e9178e6a98
parent 50694 df8ae0590be2
child 50698 49621c755075
improved Monitor_Dockable, based on ML_Statistics operations;
tuned signature;
etc/options
src/Pure/ML/ml_statistics.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/monitor_dockable.scala
     1.1 --- a/etc/options	Thu Jan 03 09:56:39 2013 +0100
     1.2 +++ b/etc/options	Thu Jan 03 13:54:45 2013 +0100
     1.3 @@ -98,3 +98,6 @@
     1.4  
     1.5  option editor_tracing_messages : int = 100
     1.6    -- "initial number of tracing messages for each command transaction"
     1.7 +
     1.8 +option editor_chart_delay : real = 3.0
     1.9 +  -- "delay for chart repainting"
     2.1 --- a/src/Pure/ML/ml_statistics.scala	Thu Jan 03 09:56:39 2013 +0100
     2.2 +++ b/src/Pure/ML/ml_statistics.scala	Thu Jan 03 13:54:45 2013 +0100
     2.3 @@ -24,6 +24,8 @@
     2.4    def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
     2.5    def apply(log: Path): ML_Statistics = apply(read_log(log))
     2.6  
     2.7 +  val empty = apply(Nil)
     2.8 +
     2.9  
    2.10    /* standard fields */
    2.11  
    2.12 @@ -84,11 +86,12 @@
    2.13  final class ML_Statistics private(val stats: List[Properties.T])
    2.14  {
    2.15    val Now = new Properties.Double("now")
    2.16 -
    2.17 -  require(!stats.isEmpty && stats.forall(props => Now.unapply(props).isDefined))
    2.18 +  def now(props: Properties.T): Double = Now.unapply(props).get
    2.19  
    2.20 -  val time_start = Now.unapply(stats.head).get
    2.21 -  val duration = Now.unapply(stats.last).get - time_start
    2.22 +  require(stats.forall(props => Now.unapply(props).isDefined))
    2.23 +
    2.24 +  val time_start = if (stats.isEmpty) 0.0 else now(stats.head)
    2.25 +  val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start
    2.26  
    2.27    val fields: Set[String] =
    2.28      SortedSet.empty[String] ++
    2.29 @@ -97,7 +100,7 @@
    2.30  
    2.31    val content: List[ML_Statistics.Entry] =
    2.32      stats.map(props => {
    2.33 -      val time = Now.unapply(props).get - time_start
    2.34 +      val time = now(props) - time_start
    2.35        require(time >= 0.0)
    2.36        val data =
    2.37          SortedMap.empty[String, Double] ++
    2.38 @@ -109,10 +112,9 @@
    2.39  
    2.40    /* charts */
    2.41  
    2.42 -  def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
    2.43 +  def update_data(data: XYSeriesCollection, selected_fields: Iterable[String])
    2.44    {
    2.45 -    val data = new XYSeriesCollection
    2.46 -
    2.47 +    data.removeAllSeries
    2.48      for {
    2.49        field <- selected_fields.iterator
    2.50        series = new XYSeries(field)
    2.51 @@ -120,20 +122,23 @@
    2.52        content.foreach(entry => series.add(entry.time, entry.data(field)))
    2.53        data.addSeries(series)
    2.54      }
    2.55 +  }
    2.56 +
    2.57 +  def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
    2.58 +  {
    2.59 +    val data = new XYSeriesCollection
    2.60 +    update_data(data, selected_fields)
    2.61  
    2.62      ChartFactory.createXYLineChart(title, "time", "value", data,
    2.63        PlotOrientation.VERTICAL, true, true, true)
    2.64    }
    2.65  
    2.66 -  def chart_panel(title: String, selected_fields: Iterable[String]): ChartPanel =
    2.67 -    new ChartPanel(chart(title, selected_fields))
    2.68 +  def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2)
    2.69  
    2.70    def standard_frames: Unit =
    2.71 -    for ((title, selected_fields) <- ML_Statistics.standard_fields) {
    2.72 -      val c = chart(title, selected_fields)
    2.73 +    ML_Statistics.standard_fields.map(chart(_)).foreach(c =>
    2.74        Swing_Thread.later {
    2.75          new Frame { contents = Component.wrap(new ChartPanel(c)); visible = true }
    2.76 -      }
    2.77 -    }
    2.78 +      })
    2.79  }
    2.80  
     3.1 --- a/src/Pure/System/session.scala	Thu Jan 03 09:56:39 2013 +0100
     3.2 +++ b/src/Pure/System/session.scala	Thu Jan 03 13:54:45 2013 +0100
     3.3 @@ -22,7 +22,7 @@
     3.4    /* events */
     3.5  
     3.6    //{{{
     3.7 -  case class Statistics(stats: Properties.T)
     3.8 +  case class Statistics(props: Properties.T)
     3.9    case class Global_Options(options: Options)
    3.10    case object Caret_Focus
    3.11    case class Raw_Edits(edits: List[Document.Edit_Text])
    3.12 @@ -361,8 +361,8 @@
    3.13              case None =>
    3.14            }
    3.15  
    3.16 -        case Markup.ML_Statistics(stats) if output.is_protocol =>
    3.17 -          statistics.event(Session.Statistics(stats))
    3.18 +        case Markup.ML_Statistics(props) if output.is_protocol =>
    3.19 +          statistics.event(Session.Statistics(props))
    3.20  
    3.21          case _ if output.is_init =>
    3.22            phase = Session.Ready
     4.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Thu Jan 03 09:56:39 2013 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Thu Jan 03 13:54:45 2013 +0100
     4.3 @@ -45,7 +45,7 @@
     4.4        "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
     4.5        "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
     4.6        "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
     4.7 -      "editor_tracing_messages", "editor_update_delay")
     4.8 +      "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")
     4.9  
    4.10    relevant_options.foreach(PIDE.options.value.check_name _)
    4.11  
     5.1 --- a/src/Tools/jEdit/src/monitor_dockable.scala	Thu Jan 03 09:56:39 2013 +0100
     5.2 +++ b/src/Tools/jEdit/src/monitor_dockable.scala	Thu Jan 03 13:54:45 2013 +0100
     5.3 @@ -12,59 +12,38 @@
     5.4  import scala.actors.Actor._
     5.5  import scala.swing.{TextArea, ScrollPane, Component}
     5.6  
     5.7 -import org.jfree.chart.{ChartFactory, ChartPanel}
     5.8 -import org.jfree.data.time.{Millisecond, TimeSeries, TimeSeriesCollection}
     5.9 +import org.jfree.chart.ChartPanel
    5.10 +import org.jfree.data.xy.XYSeriesCollection
    5.11  
    5.12  import org.gjt.sp.jedit.View
    5.13  
    5.14  
    5.15  class Monitor_Dockable(view: View, position: String) extends Dockable(view, position)
    5.16  {
    5.17 -  /* properties */  // FIXME avoid hardwired stuff
    5.18 -
    5.19 -  private val Now = new Properties.Double("now")
    5.20 -  private val Size_Heap = new Properties.Double("size_heap")
    5.21 +  /* chart data -- owned by Swing thread */
    5.22  
    5.23 -  private val series = new TimeSeries("ML heap size", classOf[Millisecond])
    5.24 -
    5.25 -
    5.26 -  /* chart */
    5.27 +  private val chart = ML_Statistics.empty.chart(null, Nil)
    5.28 +  private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
    5.29 +  private var rev_stats: List[Properties.T] = Nil
    5.30  
    5.31 -  private val chart_panel =
    5.32 -  {
    5.33 -    val data = new TimeSeriesCollection(series)
    5.34 -    val chart = ChartFactory.createTimeSeriesChart(null, "Time", "Value", data, true, true, false)
    5.35 -    val plot = chart.getXYPlot()
    5.36 +  private val delay_update =
    5.37 +    Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
    5.38 +      ML_Statistics(rev_stats.reverse)
    5.39 +        .update_data(data, ML_Statistics.tasks_fields._2)  // FIXME selectable fields
    5.40 +    }
    5.41  
    5.42 -    val x_axis = plot.getDomainAxis()
    5.43 -    x_axis.setAutoRange(true)
    5.44 -    x_axis.setFixedAutoRange(60000.0)
    5.45 -
    5.46 -    val y_axis = plot.getRangeAxis()
    5.47 -    y_axis.setAutoRange(true)
    5.48 -
    5.49 -    new ChartPanel(chart)
    5.50 -  }
    5.51 -  set_content(chart_panel)
    5.52 +  set_content(new ChartPanel(chart))
    5.53  
    5.54  
    5.55    /* main actor */
    5.56  
    5.57    private val main_actor = actor {
    5.58 -    var t0: Option[Double] = None
    5.59      loop {
    5.60        react {
    5.61 -        case Session.Statistics(stats) =>
    5.62 -          java.lang.System.err.println(stats)
    5.63 -          stats match {
    5.64 -            case Now(t1) =>
    5.65 -              if (t0.isEmpty) t0 = Some(t1)
    5.66 -              val t = t1 - t0.get
    5.67 -              stats match {
    5.68 -                case Size_Heap(x) => series.add(new Millisecond(), x)  // FIXME proper time point
    5.69 -                case _ =>
    5.70 -              }
    5.71 -            case _ =>
    5.72 +        case Session.Statistics(props) =>
    5.73 +          Swing_Thread.later {
    5.74 +            rev_stats ::= props
    5.75 +            delay_update.invoke()
    5.76            }
    5.77          case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad)
    5.78        }