--- 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"
--- 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 }
- }
- }
+ })
}
--- 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
--- 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
--- 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")
--- 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 _)
--- 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)
}