simplified time_CPU and time_GC;
derive relative speed from time (considered as step function);

--- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Fri Mar 15 10:49:28 2013 +0100
+++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Fri Mar 15 13:46:37 2013 +0100
@@ -51,10 +51,8 @@
      ("threads_wait_IO", Markup.print_int threadsWaitIO),
      ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
      ("threads_wait_signal", Markup.print_int threadsWaitSignal),
-     ("time_GC_system", signed_string_of_real (Time.toReal timeGCSystem)),
-     ("time_GC_user", signed_string_of_real (Time.toReal timeGCUser)),
-     ("time_non_GC_system", signed_string_of_real (Time.toReal timeNonGCSystem)),
-     ("time_non_GC_user", signed_string_of_real (Time.toReal timeNonGCUser))] @
+     ("time_CPU", signed_string_of_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
+     ("time_GC", signed_string_of_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
     user_counters
   end;
 

--- a/src/Pure/Tools/ml_statistics.scala	Fri Mar 15 10:49:28 2013 +0100
+++ b/src/Pure/Tools/ml_statistics.scala	Fri Mar 15 13:46:37 2013 +0100
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import scala.collection.mutable
 import scala.collection.immutable.{SortedSet, SortedMap}
 import scala.swing.{Frame, Component}
 
@@ -42,8 +43,9 @@
     ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
       "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
 
-  val time_fields =
-    ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
+  val time_fields = ("Time", List("time_CPU", "time_GC"))
+
+  val speed_fields = ("Speed", List("speed_CPU", "speed_GC"))
 
   val tasks_fields =
     ("Future tasks",
@@ -53,7 +55,8 @@
     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
 
   val standard_fields =
-    List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
+    List(GC_fields, heap_fields, threads_fields, time_fields, speed_fields,
+      tasks_fields, workers_fields)
 }
 
 final class ML_Statistics private(val name: String, val stats: List[Properties.T])
@@ -72,15 +75,34 @@
         yield x)
 
   val content: List[ML_Statistics.Entry] =
-    stats.map(props => {
+  {
+    var last_edge = Map.empty[String, (Double, Double, Double)]
+    val result = new mutable.ListBuffer[ML_Statistics.Entry]
+    for (props <- stats) {
       val time = now(props) - time_start
       require(time >= 0.0)
+
+      // rising edges -- relative speed
+      val speeds =
+        for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield {
+          val (x0, y0, s0) = last_edge.get(a) getOrElse (0.0, 0.0, 0.0)
+
+          val x1 = time
+          val y1 = java.lang.Double.parseDouble(value)
+          val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
+
+          val b = ("speed" + a).intern
+          if (y1 > y0) { last_edge += (a -> (x1, y1, s1)); (b, s1) } else (b, s0)
+        }
+
       val data =
-        SortedMap.empty[String, Double] ++
+        SortedMap.empty[String, Double] ++ speeds ++
           (for ((x, y) <- props.iterator if x != Now.name)
             yield (x, java.lang.Double.parseDouble(y)))
-      ML_Statistics.Entry(time, data)
-    })
+      result += ML_Statistics.Entry(time, data)
+    }
+    result.toList
+  }
 
 
   /* charts */