# HG changeset patch # User wenzelm # Date 1357218732 -3600 # Node ID e1df173b12a112beaca74238c2373e0a0beff520 # Parent 85f944352d55b67333e185c7a52227f9ad4081a9# Parent 373093ffcbda8de2ddb5f9f8d33fba0caa4ca65a merged diff -r 85f944352d55 -r e1df173b12a1 etc/options --- a/etc/options Thu Jan 03 13:28:37 2013 +0100 +++ b/etc/options Thu Jan 03 14:12:12 2013 +0100 @@ -53,8 +53,6 @@ -- "level of parallel proof checking: 0, 1, 2" option parallel_proofs_threshold : int = 100 -- "threshold for sub-proof parallelization" -option ML_statistics : bool = false - -- "ML runtime statistics of parallel execution environment" section "Detail of Proof Recording" @@ -98,3 +96,6 @@ option editor_tracing_messages : int = 100 -- "initial number of tracing messages for each command transaction" + +option editor_chart_delay : real = 3.0 + -- "delay for chart repainting" diff -r 85f944352d55 -r e1df173b12a1 src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala Thu Jan 03 13:28:37 2013 +0100 +++ b/src/Pure/ML/ml_statistics.scala Thu Jan 03 14:12:12 2013 +0100 @@ -24,6 +24,8 @@ def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats) def apply(log: Path): ML_Statistics = apply(read_log(log)) + val empty = apply(Nil) + /* standard fields */ @@ -84,11 +86,12 @@ final class ML_Statistics private(val stats: List[Properties.T]) { val Now = new Properties.Double("now") - - require(!stats.isEmpty && stats.forall(props => Now.unapply(props).isDefined)) + def now(props: Properties.T): Double = Now.unapply(props).get - val time_start = Now.unapply(stats.head).get - val duration = Now.unapply(stats.last).get - time_start + require(stats.forall(props => Now.unapply(props).isDefined)) + + val time_start = if (stats.isEmpty) 0.0 else now(stats.head) + val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start val fields: Set[String] = SortedSet.empty[String] ++ @@ -97,7 +100,7 @@ val content: List[ML_Statistics.Entry] = stats.map(props => { - val time = Now.unapply(props).get - time_start + val time = now(props) - time_start require(time >= 0.0) val data = SortedMap.empty[String, Double] ++ @@ -109,10 +112,9 @@ /* charts */ - def chart(title: String, selected_fields: Iterable[String]): JFreeChart = + def update_data(data: XYSeriesCollection, selected_fields: Iterable[String]) { - val data = new XYSeriesCollection - + data.removeAllSeries for { field <- selected_fields.iterator series = new XYSeries(field) @@ -120,20 +122,23 @@ content.foreach(entry => series.add(entry.time, entry.data(field))) data.addSeries(series) } + } + + def chart(title: String, selected_fields: Iterable[String]): JFreeChart = + { + val data = new XYSeriesCollection + update_data(data, selected_fields) ChartFactory.createXYLineChart(title, "time", "value", data, PlotOrientation.VERTICAL, true, true, true) } - def chart_panel(title: String, selected_fields: Iterable[String]): ChartPanel = - new ChartPanel(chart(title, selected_fields)) + def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2) def standard_frames: Unit = - for ((title, selected_fields) <- ML_Statistics.standard_fields) { - val c = chart(title, selected_fields) + ML_Statistics.standard_fields.map(chart(_)).foreach(c => Swing_Thread.later { new Frame { contents = Component.wrap(new ChartPanel(c)); visible = true } - } - } + }) } diff -r 85f944352d55 -r e1df173b12a1 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Thu Jan 03 13:28:37 2013 +0100 +++ b/src/Pure/System/isabelle_process.ML Thu Jan 03 14:12:12 2013 +0100 @@ -238,7 +238,7 @@ protocol_command "Isabelle_Process.options" (fn [options_yxml] => let val options = Options.decode (YXML.parse_body options_yxml) in - Future.ML_statistics := Options.bool options "ML_statistics"; + Future.ML_statistics := true; Multithreading.trace := Options.int options "threads_trace"; Multithreading.max_threads := Options.int options "threads"; if Multithreading.max_threads_value () < 2 diff -r 85f944352d55 -r e1df173b12a1 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Jan 03 13:28:37 2013 +0100 +++ b/src/Pure/System/session.scala Thu Jan 03 14:12:12 2013 +0100 @@ -22,7 +22,7 @@ /* events */ //{{{ - case class Statistics(stats: Properties.T) + case class Statistics(props: Properties.T) case class Global_Options(options: Options) case object Caret_Focus case class Raw_Edits(edits: List[Document.Edit_Text]) @@ -361,8 +361,8 @@ case None => } - case Markup.ML_Statistics(stats) if output.is_protocol => - statistics.event(Session.Statistics(stats)) + case Markup.ML_Statistics(props) if output.is_protocol => + statistics.event(Session.Statistics(props)) case _ if output.is_init => phase = Session.Ready diff -r 85f944352d55 -r e1df173b12a1 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Thu Jan 03 13:28:37 2013 +0100 +++ b/src/Pure/Tools/build.ML Thu Jan 03 14:12:12 2013 +0100 @@ -43,7 +43,7 @@ (Options.int options "parallel_proofs_threshold") |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace") |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads") - |> Unsynchronized.setmp Future.ML_statistics (Options.bool options "ML_statistics") + |> Unsynchronized.setmp Future.ML_statistics true |> no_document options ? Present.no_document |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty") |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs") diff -r 85f944352d55 -r e1df173b12a1 src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Thu Jan 03 13:28:37 2013 +0100 +++ b/src/Tools/jEdit/src/isabelle_options.scala Thu Jan 03 14:12:12 2013 +0100 @@ -43,9 +43,9 @@ private val relevant_options = Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin", - "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics", + "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit", - "editor_tracing_messages", "editor_update_delay") + "editor_tracing_messages", "editor_update_delay", "editor_chart_delay") relevant_options.foreach(PIDE.options.value.check_name _) diff -r 85f944352d55 -r e1df173b12a1 src/Tools/jEdit/src/monitor_dockable.scala --- a/src/Tools/jEdit/src/monitor_dockable.scala Thu Jan 03 13:28:37 2013 +0100 +++ b/src/Tools/jEdit/src/monitor_dockable.scala Thu Jan 03 14:12:12 2013 +0100 @@ -12,59 +12,38 @@ import scala.actors.Actor._ import scala.swing.{TextArea, ScrollPane, Component} -import org.jfree.chart.{ChartFactory, ChartPanel} -import org.jfree.data.time.{Millisecond, TimeSeries, TimeSeriesCollection} +import org.jfree.chart.ChartPanel +import org.jfree.data.xy.XYSeriesCollection import org.gjt.sp.jedit.View class Monitor_Dockable(view: View, position: String) extends Dockable(view, position) { - /* properties */ // FIXME avoid hardwired stuff - - private val Now = new Properties.Double("now") - private val Size_Heap = new Properties.Double("size_heap") + /* chart data -- owned by Swing thread */ - private val series = new TimeSeries("ML heap size", classOf[Millisecond]) - - - /* chart */ + private val chart = ML_Statistics.empty.chart(null, Nil) + private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection] + private var rev_stats: List[Properties.T] = Nil - private val chart_panel = - { - val data = new TimeSeriesCollection(series) - val chart = ChartFactory.createTimeSeriesChart(null, "Time", "Value", data, true, true, false) - val plot = chart.getXYPlot() + private val delay_update = + Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { + ML_Statistics(rev_stats.reverse) + .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields + } - val x_axis = plot.getDomainAxis() - x_axis.setAutoRange(true) - x_axis.setFixedAutoRange(60000.0) - - val y_axis = plot.getRangeAxis() - y_axis.setAutoRange(true) - - new ChartPanel(chart) - } - set_content(chart_panel) + set_content(new ChartPanel(chart)) /* main actor */ private val main_actor = actor { - var t0: Option[Double] = None loop { react { - case Session.Statistics(stats) => - java.lang.System.err.println(stats) - stats match { - case Now(t1) => - if (t0.isEmpty) t0 = Some(t1) - val t = t1 - t0.get - stats match { - case Size_Heap(x) => series.add(new Millisecond(), x) // FIXME proper time point - case _ => - } - case _ => + case Session.Statistics(props) => + Swing_Thread.later { + rev_stats ::= props + delay_update.invoke() } case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad) }