# HG changeset patch
# User wenzelm
# Date 1357156967 -3600
# Node ID 0607d557d073591e3939b08d2b9e6456ec82f402
# Parent  f02864682307d52de4c5204af9f55c1dadf073a9
some support for chart drawing;

diff -r f02864682307 -r 0607d557d073 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed Jan 02 19:23:18 2013 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Wed Jan 02 21:02:47 2013 +0100
@@ -9,6 +9,10 @@
 
 import scala.collection.immutable.{SortedSet, SortedMap}
 
+import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
+import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
+import org.jfree.chart.plot.PlotOrientation
+
 
 object ML_Statistics
 {
@@ -59,7 +63,7 @@
   val time_start = ML_Statistics.Now.unapply(stats.head).get
   val duration = ML_Statistics.Now.unapply(stats.last).get - time_start
 
-  val names: Set[String] =
+  val fields: Set[String] =
     SortedSet.empty[String] ++
       (for (props <- stats.iterator; (x, _) <- props.iterator if x != ML_Statistics.Now.name)
         yield x)
@@ -74,5 +78,27 @@
             yield (x, java.lang.Double.parseDouble(y)))
       ML_Statistics.Entry(time, data)
     })
+
+
+  /* charts */
+
+  def chart(title: String, selected_fields: String*): JFreeChart =
+  {
+    val data = new XYSeriesCollection
+
+    for {
+      field <- selected_fields
+      series = new XYSeries(field)
+    } {
+      content.foreach(entry => series.add(entry.time, entry.data(field)))
+      data.addSeries(series)
+    }
+
+    ChartFactory.createXYLineChart(title, "time", "value", data,
+      PlotOrientation.VERTICAL, true, true, true)
+  }
+
+  def chart_panel(title: String, selected_fields: String*): ChartPanel =
+    new ChartPanel(chart(title, selected_fields: _*))
 }
 
diff -r f02864682307 -r 0607d557d073 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Jan 02 19:23:18 2013 +0100
+++ b/src/Pure/build-jars	Wed Jan 02 21:02:47 2013 +0100
@@ -126,6 +126,15 @@
 [ "$#" -ne 0 ] && usage
 
 
+## dependencies
+
+declare -a JFREECHART_JARS=()
+for NAME in $JFREECHART_JAR_NAMES
+do
+  JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
+done
+
+
 ## build
 
 TARGET_DIR="$ISABELLE_HOME/lib/classes"
@@ -182,18 +191,23 @@
 
   JFXRT="$ISABELLE_JDK_HOME/jre/lib/jfxrt.jar"
 
-  if [ "$TEST_PIDE" = true ]; then
-    isabelle_scala scalac $SCALAC_OPTIONS \
-        -classpath "$(jvmpath "$JFXRT:classes")" "${PIDE_SOURCES[@]}" || \
-      fail "Failed to compile PIDE sources"
-    isabelle_scala scalac $SCALAC_OPTIONS \
-        -classpath "$(jvmpath "$JFXRT:classes")" "${PURE_SOURCES[@]}" || \
-      fail "Failed to compile Pure sources"
-  else
-    isabelle_scala scalac $SCALAC_OPTIONS \
-        -classpath "$(jvmpath "$JFXRT:classes")" "${PIDE_SOURCES[@]}" "${PURE_SOURCES[@]}" || \
-      fail "Failed to compile sources"
-  fi
+  (
+    for X in "$JFXRT" "${JFREECHART_JARS[@]}" classes
+    do
+      CLASSPATH="$CLASSPATH:$X"
+    done
+    CLASSPATH="$(jvmpath "$CLASSPATH")"
+
+    if [ "$TEST_PIDE" = true ]; then
+      isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
+        fail "Failed to compile PIDE sources"
+      isabelle_scala scalac $SCALAC_OPTIONS "${PURE_SOURCES[@]}" || \
+        fail "Failed to compile Pure sources"
+    else
+      isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" "${PURE_SOURCES[@]}" || \
+        fail "Failed to compile sources"
+    fi
+  )
 
   mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext"